Logical derivation of computer programs
By: Thomas G. Windeknecht.
Publisher: Intellect
Published: 1999
Place of publication: Exeter, England
Language: eng
Number of pages: 208
Subjects: Computer programming -- Mathematics.
Notes: Includes bibliographical references (p. 179-180) and index.
Table of contents: title: Machine generated contents note: 1 Logical Proofs; title: 1.1 BACKGROUND 1; title: 1.2 LOGICAL PROOF SYSTEMS 2; title: 1.3 PROOFS IN BOOLEAN ALGEBRA5; title: 1.4 PROVING PROPOSITIONAL CALCULUS 10; title: 1.5 TAUTOLOGIES13; title: 1.6 OTHER FORMS OF LOGICAL PROOF 14; title: 1.7 QUANTIFIERS 16; title: 1.8 FOUR AXIOMS OF SET THEORY 20; title: 1.9 SET-THEORETIC IDENTITIES 22; title: 1.10 PROVING THE ALGEBRA OF SETS 24; title: 1.11 DECOMPOSITION OF PROOFS 29; title: EXERCISES 33; title: 2 Mathematical Induction; title: 2.1 THE SET OF NATURAL NUMBERS 37; title: 2.2 DEFINING ARITHMETIC 41; title: 2.3 HIGHER-ORDER INDUCTIVE DEFINITIONS 45; title: 2.4 EVOLVERS AND ITERATION 47; title: 2.5 SET-THEORETIC EVOLVERS 50; title: 2.6 THE ALGEBRA OF RELATIONS52; title: 2.7 INDUCTIVE PROOFS 54; title: 2.8 THE ALGEBRA OF LISTS58; title: EXERCISES 61; title: 3 Traditional Programming; title: 3.1 INTRODUCTION 65; title: 3.2 A RUDIMENTARY PROGRAMMING LANGUAGE 67; title: 3.3 INVENTION OF PROGRAMS 69; title: 3.4 FORMALIZING PROCEDURAL SPECIFICATIONS 74; title: 3.5 INFORMAL VERIFICATION ARGUMENTS76; title: EXERCISES 79; title: 4 A Logic for Procedures; title: 4.1 INTRODUCTION. 83; title: 4.2 PROCEDURAL EQUIVALENCE 84; title: 4.3 THE SUBSTITUTION AND LEIBNITZ RULES 86; title: 4.4 REWRITING RULES FOR ASSIGNMENTS90; title: 4.5 CONDITIONAL EXPRESSIONS AND BRANCHES 95; title: 4.6 ITERATION AND FOR-LOOPS99; title: 4.7 HIGH-LEVEL REWRITING RULES 103; title: 4.8 RECURSIVE PROCEDURES 109; title: 4.9 TAIL RECURSION AND WHILE-LOOPS 113; title: 4.10 PROGRAMS AND PROCEDURE CALL REPLACEMENT 117; title: EXERCISES 122; title: 5 Examples of Program Derivation; title: 5.1 PROGRAMMING THE ALGEBRA OF SETS127; title: 5.2 PROGRAMMING PREDICATES 132; title: 5.3 PROGRAMMING THE ALGEBRA OF RELATIONS 139; title: 5.4 PROGRAMMING EQUIVALENCE RELATIONS AND PARTITIONS 144; title: 5.5 PROGRAMMING THE TRANSITIVE CLOSURE 149; title: 5.6 EMBEDDING SPECIFICATIONS 151; title: 5.7 PROGRAMMING NATURAL NUMBER ARITHMETIC 152; title: 5.8 PROGRAMMING THE ALGEBRA OF LISTS 161; title: 5.9 COMPUTING SETS USING ONE-ONE LISTS 164; title: 5.10 SEARCHING AND SORTING LISTS 167; title: EXERCISES 174.