Inventory of Reasoning about Correctness (IRC) Principles

The purpose of this inventory is to identify the basic set of principles that are central for analytical reasoning
about correctness of software and that must be taught in undergraduate computing education.

Major Reasoning Topic	Subtopic Summary	Concept Term Highlights	Concept Details
1. Logic	1.1. Motivation	1.1.1. Motivation for Boolean Logic
	1.2. Standard logic symbols	1.2.1. Connectives including implication 1.2.2. Quantifiers	1.2.1.1. Simple statement 1.2.1.2. Connectives ( NOT, AND, OR, IF... THEN, IFF) and compound statements 1.2.1.3. Truth tables 1.2.1.4. Logically equivalent statements 1.2.2.1. Universal quantifier 1.2.2.2. Existential quantifier
	1.3. Standard terminology	1.3.1. Proposition 1.3.2. Predicate logic 1.3.3. Proof	1.3.1.1. Propositional variables 1.3.1.2. Compound propositions 1.3.1.3. Proof arguments 1.3.2.1. Predicate calculus 1.3.3.1. Informal proof 1.3.3.2. Axiom 1.3.3.3. Premise 1.3.3.4. Conclusion
	1.4. Standard proof techniques	1.4.1. Supposition Deduction
	1.5. Methods for proving	1.5.1. Direct proof 1.5.2. Proof by contradiction 1.5.3. Vacuous proof 1.5.4. Trivial proof 1.5.5. Proof by cases 1.5.6. Exhaustive proof 1.5.7. Proof by induction
	1.6. Proof strategies	1.6.1. Forward reasoning 1.6.2. Backward reasoning
	1.7. Rules of inference	1.7.1. Modus ponens 1.7.2. Simplification Conjunction 1.7.3. Universal instantiation 1.7.4. Universal generalization 1.7.5. Existential instantiation 1.7.6. Existential generalization
2. Discrete Math Structures	2.1. Motivation	2.1.1. Motivation for Discrete Mathematics
	2.2. Sets	2.2.1. Set basics 2.2.2. Set notations 2.2.3. Laws of Algebra on Sets	2.2.1.1. Set naming conventions 2.2.1.2. Universal set U 2.2.1.3. Empty set ϕ 2.2.1.4. Element naming conventions 2.2.1.5. Subset 2.2.1.6. Subset Theorem 2.2.1.7. Venn diagrams 2.2.2.1. Union 2.2.2.2. Intersection 2.2.2.3. Disjoint sets 2.2.2.4. Relative Compliment 2.2.2.5. Absolute Compliment 2.2.2.6. Power set 2.2.2.7. Power set for a finite set 2.2.2.8. Cartesian product 2.2.2.9. Extensibility over finite set 2.2.2.10. Cartesian product of a set on itself 2.2.3.1. Idempotent Laws 2.2.3.2. Associative Laws 2.2.3.3. Commutative Laws 2.2.3.4. Distributive Laws 2.2.3.5. Identity Laws 2.2.3.6. Involution Law 2.2.3.7. Complement Laws 2.2.3.8. DeMorgan's Lawss
	2.3. Strings	2.3.1. String basics 2.3.2. String notations and Properties	2.3.1.1. String variable name conventions 2.3.1.2. Alphabet set Σ 2.3.1.3. Strings over the alphabet set Σ* 2.3.2.1. Empty string 2.3.2.1. String length 2.3.2.1. Concatenation 2.3.2.1. String reversal 2.3.2.1. Substring
	2.4. Numbers	2.4.1. Number Representations	2.4.1.1. Number notations 2.4.1.2. Number bases
	2.5. Relations and Functions	2.5.1. Relations 2.5.2. Functions	2.5.1.1. Relation notation 2.5.1.2. Inverse relations 2.5.1.3. Composition of Relations 2.5.1.4. Reflexive property 2.5.1.5. Symmetric property 2.5.1.6. Anti-symmetric property 2.5.1.7. Transitive property 2.5.1.8. Atransitive property 2.5.1.9. Equivalence Relation 2.5.2.1. Function notation 2.5.2.2. Domain and codomain 2.5.2.3. Dependent and independent variables 2.5.2.4. Equal functions 2.5.2.5. Cartesian coordinate system 2.5.2.6. Injective function 2.5.2.7. Surjective function 2.5.2.8. Bijective function
	2.6. Graph Theory	2.7.1. Graph Basics 2.7.2. Graph Types	2.7.1.1. Graph notations 2.7.1.2. Edges and vertices 2.7.1.3. Degree of a vertex 2.7.1.4. Graph representation 2.7.1.5. Tree and forest 2.7.2.1. Multigraphs 2.7.2.2. Finite graphs 2.7.2.3. Complete graphs 2.7.2.4. k-regular graphs 2.7.2.5. Acyclic graph 2.7.2.6. Planar graphs
	2.7. Permutations and Combinations	2.7.1. Notations	2.7.1.1. Permutation notation 2.7.1.2. Factorial notation 2.7.1.3. Combinations notation
3. Precise Specifications (Mathematical descriptions of interfaces)	3.1. Motivation	3.1.1. Motivation for interfaces 3.1.2. Motivation for precision		3.1.1.1. Information hiding 3.1.1.2. Independent software development 3.1.2.1. Problems with informal specifications 3.1.2.2. Ease of component integration
	3.2. Specification structure	3.2.1. Specification signature 3.2.2. Usage Requirements 3.2.3. Use of math theories 3.2.4. Specification inheritance (enhancements)		3.2.1.1. Concept name 3.2.1.2. Generic parameters
	3.3. Abstraction	3.3.1. Math models for conceptualizing objects 3.3.2. Constraints 3.3.3. Trade-offs of alternative mathematical models		3.3.1.1. Booleans 3.3.1.2. Numbers 3.3.1.3. Integers 3.3.1.4. Strings 3.3.1.5. Sets 3.3.1.6. Functions 3.3.1.7. Relations 3.3.1.8. Cartesian products 3.3.1.9. Other discrete structures 3.3.1.10. Combination of the above
	3.4. Specifications of operations	3.4.1. Initialization and finalization specification 3.4.2. Operation signature 3.4.3. Pre- and post- conditions		3.4.2.1. Operation Name 3.4.2.2. Formal parameters 3.4.2.3. Return Value 3.4.3.1. Specification parameter modes 3.4.3.2. Responsibility of the caller 3.4.3.3. Responsibility of the Implementer 3.4.3.4. Equivalent specifications 3.4.3.5. Redundant Specifications 3.4.3.6. Notation to distinguish an incoming value in the post-condition
4. Modular Reasoning	4.1. Motivation	4.1.1. Motivation for Reasoning 4.1.2. Motivation for Modular Reasoning		4.1.1.1. Error detection 4.1.1.2. Code tracing/inspection 4.1.1.3. Formal Verification 4.1.2.1. Problems with implementation to implementation coupling 4.1.2.2. Desirable coupling through contracts
	4.2. Design-by-Contract	4.2.1. Roles of clients and service providers 4.2.2. Construction of new components from built-in components 4.2.3. Construction of new components using existing components		4.2.1.1. Specifications as external contracts 4.2.1.2. Client 4.2.1.3. Service Provider 4.2.1.4. Client implementation 4.2.1.5. Service provider implementation 4.2.2.1. Implementation with arrays 4.2.2.2. Implementation with records 4.2.3.1. Implementation of a specification (data representation, code for operations) 4.2.3.2. Implementation of enhancement specification
	4.3. Internal contracts and Assertions	4.3.1. Internal contracts for data representations 4.3.2. Assertions		4.3.1.1. Abstraction functions/ relations (correspondence) 4.3.1.2. Representation invariants (conventions) 4.3.2.1. Loop invariants 4.3.2.2. Progress metrics (loops and recursive procedures)
5. Correctness Proofs	5.1. Motivation	5.1.1. Meaning of correctness 5.1.2. Motivation for proofs		5.1.1.1. Semantics 5.1.1.2. Soundness and relative completeness 5.1.2.1. Partial correctness 5.1.2.2. Total correctness
	5.2.Construction of verification Conditions (VCs)	5.2.1. States and abstract values of objects 5.2.2. Connection between specifications and what is to be proved 5.2.3. Types of Statements 5.2.4. Connection between induction and reasoning		5.2.1.1. Naming conventions 5.2.2.1. Assumptions 5.2.2.2. Obligations 5.2.3.1. Sequential statements 5.2.3.2. Conditional statements 5.2.3.3. Loops 5.2.3.4. Operation calls 5.2.4.1. Inductive case 5.2.4.2. Base case 5.2.4.3. Termination
	5.3. Proof of VCs	5.3.1. VCs as mathematical implications 5.3.2. Application of proof techniques on VCs		5.3.1.1. Givens 5.3.1.2. Goals 5.3.2.1. Direct proofs 5.3.2.2. Rules of inference