Programming,2019 12 21 edition,Eric C R Hehner,Department of Computer Science. University of Toronto,Toronto ON M5S 2E4 Canada,The first edition of this book was published by. Springer Verlag Publishers New York 1993,ISBN 0 387 94106 1 QA76 6 H428. The current edition is available free at,www cs utoronto ca hehner aPToP. An on line course based on this book is at,www cs utoronto ca hehner FMSD. The author s website is,www cs utoronto ca hehner, You may copy all or part of this book freely as long as you include this page. The cover picture is an inukshuk which is a human like figure made of piled stones. Inukshuks are found throughout arctic Canada They are built by the Inuit people. who use them to mean You are on the right path,0 Introduction 0. 0 0 Current Edition 1,0 1 Quick Tour 1,0 2 Acknowledgements 2. 1 Basic Theories 3,1 0 Binary Theory 3,1 0 0 Axioms and Proof Rules 5. 1 0 1 Expression and Proof Format 7,1 0 2 Monotonicity and Antimonotonicity 9. 1 0 3 Context 10,1 0 4 Formalization 12,1 1 Number Theory 12. 1 2 Character Theory 13,2 Basic Data Structures 14. 2 0 Bunch Theory 14,2 1 Set Theory optional 17,2 2 String Theory 17. 2 3 List Theory 20,2 3 0 Multidimensional Structures 22. 3 Function Theory 23,3 0 Functions 23,3 0 0 Abbreviated Function Notations 25. 3 0 1 Scope and Substitution 25,3 1 Quantifiers 26. 3 2 Function Fine Points optional 29,3 2 0 Function Inclusion and Equality optional 30. 3 2 1 Higher Order Functions optional 30,3 2 2 Function Composition optional 31. 3 3 List as Function 32,3 4 Limits and Reals optional 33. 4 Program Theory 34,4 0 Specifications 34,4 0 0 Specification Notations 36. 4 0 1 Specification Laws 37,4 0 2 Refinement 39,4 0 3 Conditions optional 40. 4 0 4 Programs 41,4 1 Program Development 43,4 1 0 Refinement Laws 43. 4 1 1 List Summation 43,4 1 2 Binary Exponentiation 45. 3 Contents,4 2 Time 46,4 2 0 Real Time 46,4 2 1 Recursive Time 48. 4 2 2 Termination 50,4 2 3 Soundness and Completeness optional 51. 4 2 4 Linear Search 51,4 2 5 Binary Search 53,4 2 6 Fast Exponentiation 57. 4 2 7 Fibonacci Numbers 59,4 3 Space 61,4 3 0 Maximum Space 63. 4 3 1 Average Space 64,5 Programming Language 66,5 0 Scope 66. 5 0 0 Variable Declaration 66,5 0 1 Variable Suspension 67. 5 1 Data Structures 68,5 1 0 Array 68,5 1 1 Record 69. 5 2 Control Structures 69,5 2 0 While Loop 69,5 2 1 Loop with Exit 71. 5 2 2 Two Dimensional Search 72,5 2 3 For Loop 74,5 2 4 Go To 75. 5 3 Time and Space Dependence 76,5 4 Assertions optional 77. 5 4 0 Checking 77,5 4 1 Backtracking 77,5 5 Subprograms 78. 5 5 0 Result Expression 78,5 5 1 Function 79,5 5 2 Procedure 80. 5 6 Alias optional 81,5 7 Probabilistic Programming optional 82. 5 7 0 Random Number Generators 84,5 7 1 Information optional 87. 5 8 Functional Programming optional 88,5 8 0 Function Refinement 89. 6 Recursive Definition 91,6 0 Recursive Data Definition 91. 6 0 0 Construction and Induction 91,6 0 1 Least Fixed Points 94. 6 0 2 Recursive Data Construction 95,6 1 Recursive Program Definition 97. 6 1 0 Recursive Program Construction 98,6 1 1 Loop Definition 99. Contents 2,7 Theory Design and Implementation 100,7 0 Data Theories 100. 7 0 0 Data Stack Theory 100,7 0 1 Data Stack Implementation 101. 7 0 2 Simple Data Stack Theory 102,7 0 3 Data Queue Theory 103. 7 0 4 Data Tree Theory 104,7 0 5 Data Tree Implementation 104. 7 1 Program Theories 106,7 1 0 Program Stack Theory 106. 7 1 1 Program Stack Implementation 106,7 1 2 Fancy Program Stack Theory 107. 7 1 3 Weak Program Stack Theory 107,7 1 4 Program Queue Theory 108. 7 1 5 Program Tree Theory 108,7 2 Data Transformation 109. 7 2 0 Security Switch 111,7 2 1 Take a Number 112,7 2 2 Parsing 113. 7 2 3 Limited Queue 115,7 2 4 Soundness and Completeness optional 117. 8 Concurrency 118,8 0 Independent Composition 118,8 0 0 Laws of Independent Composition 120. 8 0 1 List Concurrency 120,8 1 Sequential to Parallel Transformation 121. 8 1 0 Buffer 122,8 1 1 Insertion Sort 123,8 1 2 Dining Philosophers 124. 9 Interaction 126,9 0 Interactive Variables 126,9 0 0 Thermostat 128. 9 0 1 Space 129,9 1 Communication 131,9 1 0 Implementability 132. 9 1 1 Input and Output 133,9 1 2 Communication Timing 134. 9 1 3 Recursive Communication optional 134,9 1 4 Merge 135. 9 1 5 Monitor 136,9 1 6 Reaction Controller 137,9 1 7 Channel Declaration 138. 9 1 8 Deadlock 139,9 1 9 Broadcast 140,1 Contents,10 Exercises 147. 10 0 Introduction 147,10 1 Basic Theories 147,10 2 Basic Data Structures 155. 10 3 Function Theory 157,10 4 Program Theory 162,10 5 Programming Language 181. 10 6 Recursive Definition 187,10 7 Theory Design and Implementation 194. 10 8 Concurrency 201,10 9 Interaction 204,11 Reference 209. 11 0 Justifications 209,11 0 0 Notation 209,11 0 1 Basic Theories 209. 11 0 2 Basic Data Structures 210,11 0 3 Function Theory 212. 11 0 4 Program Theory 212,11 0 5 Programming Language 214. 11 0 6 Recursive Definition 215,11 0 7 Theory Design and Implementation 215. 11 0 8 Concurrency 216,11 0 9 Interaction 216,11 1 Sources 217. 11 2 Bibliography 219,11 3 Index 223,11 4 Laws 231. 11 4 0 Binary 231,11 4 1 Generic 233,11 4 2 Numbers 233. 11 4 3 Bunches 234,11 4 4 Sets 235,11 4 5 Strings 235. 11 4 6 Lists 236,11 4 7 Functions 236,11 4 8 Quantifiers 237. 11 4 9 Limits 239,11 4 10 Specifications and Programs 239. 11 4 11 Substitution 240,11 4 12 Conditions 240,11 4 13 Refinement 240. 11 5 Names 241,11 6 Symbols 242,11 7 Precedence 243. 11 8 Distribution 243,End of Contents,0 Introduction. What good is a theory of programming Who wants one Thousands of programmers program. every day without any theory Why should they bother to learn one The answer is the same as for. any other theory For example why should anyone learn a theory of motion You can move. around perfectly well without one You can throw a ball without one Yet we think it important. enough to teach a theory of motion in high school, One answer is that a mathematical theory gives a much greater degree of precision by providing a. method of calculation It is unlikely that we could send a rocket to Jupiter without a mathematical. theory of motion And even baseball pitchers are finding that their pitch can be improved by using. some theory Similarly a lot of mundane programming can be done without the aid of a theory but. the more difficult programming is very unlikely to be done correctly without a good theory The. software industry has an overwhelming experience of buggy programs to support that statement. And even mundane programming can be improved by the use of a theory. Another answer is that a theory provides a kind of understanding Our ability to control and predict. motion changes from an art to a science when we learn a mathematical theory Similarly. programming changes from an art to a science when we learn to understand programs in the same. way we understand mathematical theorems With a scientific outlook we change our view of the. world We attribute less to spirits or chance and increase our understanding of what is possible. and what is not It is a valuable part of education for anyone. Professional engineering maintains its high reputation in our society by insisting that to be a. professional engineer one must know and apply the relevant theories A civil engineer must know. and apply the theories of geometry and material stress An electrical engineer must know and apply. electromagnetic theory Software engineers to be worthy of the name must know and apply a. theory of programming, The subject of this book sometimes goes by the name programming methodology science of. programming logic of programming theory of programming formal methods of. program development or verification It concerns those aspects of programming that are. amenable to mathematical proof A good theory helps us to write precise specifications and to. design programs whose executions provably satisfy the specifications We will be considering the. state of a computation the time of a computation the memory space required by a computation and. the interactions with a computation There are other important aspects of software design and. production that are not touched by this book the management of people the user interface. documentation and testing, In the first usable theory of programming often called Hoare s Logic a specification is a pair of. predicates a precondition and postcondition these and all technical terms will be defined in due. course A closely related theory uses Dijkstra s weakest precondition predicate transformer which. is a function from programs and postconditions to preconditions further advanced in Back s. Refinement Calculus Jones s Vienna Development Method has been used to advantage in some. industries in it a specification is a pair of predicates as in Hoare s Logic but the second predicate. is a relation There are theories that specialize in real time programming some in probabilistic. programming some in interactive programming,1 0 Introduction. The theory in this book is simpler than any of those just mentioned In it a specification is just a. binary expression Refinement is just ordinary implication This theory is also more. comprehensive than those just mentioned applying to both terminating and nonterminating. computation to both sequential and parallel computation to both stand alone and interactive. computation All at the same time we can have variables whose initial and final values are all that is. of interest variables whose values are continuously of interest variables whose values are known. only probabilistically and variables that account for time and space They all fit together in one. theory whose basis is the standard scientific practice of writing a specification as a binary. expression whose nonlocal variables represent whatever is considered to be of interest. There is an approach to program proving that exhaustively tests all inputs called model checking. Its advantage over the theory in this book is that it is fully automated With a clever representation. of binary expressions see Exercise 15 model checking currently boasts that it can explore up to. about 1060 states That is something like the number of atoms in our galaxy It is an impressive. number until we realize that 1060 is about 2 200 which means we are talking about 200 bits. That is the state space of six 32 bit variables To use model checking on any program with more. than six variables requires abstraction and each abstraction requires proof that it preserves the. properties of interest These abstractions and proofs are not automatic To be practical model. checking must be joined with other methods of proving such as those in this book. The emphasis throughout this book is on program development with proof at each step rather than. on proof after development, An on line course based on this book is at www cs utoronto ca hehner FMSD Solutions to. exercises are at www cs utoronto ca hehner aPToP solutions. 0 0 Current Edition, Since the first edition of this book new material has been added on space bounds and on. probabilistic programming The for loop rule has been generalized The treatment of concurrency. has been simplified And for cooperation between parallel processes there is now a choice. communication as in the first edition and interactive variables which are the formally tractable. version of shared memory Explanations have been improved throughout the book and more. worked examples have been added As well as additions there have been deletions Any material. that was usually skipped in a course has been removed to keep the book short It s really only 147. pages after that is just exercises and reference material. The complete log of changes to the book is at www cs utoronto ca hehner aPToP changelog pdf. End of Current Edition,0 1 Quick Tour, All technical terms used in this book are explained in this book Each new term that you should. learn is underlined The terminology is descriptive rather than honorary For example the data. type with two values is called binary rather than boolean the former word describes the data. type the latter word honors George Boole There are no abbreviations acronyms or other. obscurities of language to annoy you No specific previous mathematical knowledge or. programming experience is assumed However the preparatory material on binary values numbers. lists and functions in Chapters 1 2 and 3 is brief and previous exposure might be helpful. 0 Introduction 2, The following chart shows the dependence of each chapter on previous chapters. 1 2 3 4 6 7, Chapter 4 Program Theory is the heart of the book After that chapters may be selected or omitted. according to interest and the chart The only deviations from the chart are that Chapter 9 uses. variable declaration presented in Subsection 5 0 0 and small optional Subsection 9 1 3 depends on. Chapter 6 Within each chapter sections and subsections marked as optional can be omitted. without much harm to the following material, Chapter 10 consists entirely of exercises grouped according to the chapter in which the necessary. theory is presented All the exercises in the section Program Theory can be done according to. the methods presented in Chapter 4 however as new methods are presented in later chapters those. same exercises can be redone taking advantage of the later material. At the back of the book Chapter 11 contains reference material Section 11 0 Justifications. answers questions about earlier chapters such as why was this presented that way why was this. presented at all why wasn t something else presented instead It may be of interest to teachers and. researchers who already know enough theory of programming to ask such questions It is. probably not of interest to students who are meeting formal methods for the first time If you find. yourself asking such questions don t hesitate to consult the justifications. Chapter 11 also contains an index of terminology and a complete list of all laws used in the book. To a serious student of programming these laws should become friends on a first name basis The. final pages list all the notations used in the book You are not expected to know these notations. before reading the book they are all explained as we come to them You are welcome to invent. new notations if you explain their use Sometimes the choice of notation makes all the difference in. our ability to solve a problem,End of Quick Tour,0 2 Acknowledgements. For inspiration and guidance I thank Working Group 2 3 Programming Methodology of the. International Federation for Information Processing particularly Edsger Dijkstra David Gries. Tony Hoare Jim Horning Cliff Jones Bill McKeeman Jay Misra Carroll Morgan Greg Nelson. John Reynolds and Wlad Turski I especially thank Doug McIlroy for encouragement I thank. my graduate students and teaching assistants from whom I have learned so much especially Lorene. Gupta Peter Kanareitsev Yannis Kassios Victor Kwan Albert Lai Chris Lengauer Andrew. Malton Lev Naiman Theo Norvell Rich Paige Hugh Redelmeier Alan Rosenthal Anya Tafliovich. Justin Ward and Robert Will For their critical and helpful reading of the first draft I am most. grateful to Wim Hesselink Jim Horning and Jan van de Snepscheut For good ideas I thank Ralph. Back Wim Feijen Netty van Gasteren Nicolas Halbwachs Gilles Kahn Leslie Lamport Alain. Martin Joe Morris Martin Rem Pierre Yves Schobbens Mary Shaw Bob Tennent and Jan Tijmen. Udding For reading the draft and suggesting improvements I thank Jules Desharnais Andy. Gravell Ali Mili Bernhard M ller Helmut Partsch J rgen Steensgaard Madsen and Norbert. V lker I thank my classes for finding errors,End of Acknowledgements. End of Introduction,1 Basic Theories, The basic theories we need are Binary Theory Number Theory and Character Theory. 1 0 Binary Theory, Binary Theory also known as boolean algebra or logic was designed as an aid to reasoning and. we will use it to reason about computation The expressions of Binary Theory are called binary. expressions We call some binary expressions theorems and others antitheorems. The expressions of Binary Theory can be used to represent statements about the world the. theorems represent true statements and the antitheorems represent false statements That is the. original application of the theory the one it was designed for and the one that supplies most of the. terminology Another application for which Binary Theory is perfectly suited is digital circuit. design In that application binary expressions represent circuits theorems represent circuits with. high voltage output and antitheorems represent circuits with low voltage output In general Binary. Theory can be used for any application that has two values. The two simplest binary expressions are T and The first one T is a theorem and the. second one is an antitheorem When Binary Theory is being used for its original purpose we. pronounce T as true and as false because the former represents an arbitrary true. statement and the latter represents an arbitrary false statement When Binary Theory is being used. for digital circuit design we pronounce T and as high voltage and low voltage or as. power and ground Similarly we may choose words from other application areas Or to be. independent of application we may call them top and bottom They are the zero operand. binary operators because they have no operands, There are four one operand binary operators of which only one is interesting Its symbol is. pronounced not It is a prefix operator placed before its operand An expression of the form. x is called a negation If we negate a theorem we obtain an antitheorem if we negate an. antitheorem we obtain a theorem This is depicted by the following truth table. Above the horizontal line T means that the operand is a theorem and means that the operand is. an antitheorem Below the horizontal line T means that the result is a theorem and means that. the result is an antitheorem, There are sixteen two operand binary operators Mainly due to tradition we will use only six of. them though they are not the only interesting ones These operators are infix placed between their. operands Here are the symbols and some pronunciations. implies is equal to or stronger than, follows from is implied by is weaker than or equal to. equals if and only if, differs from is unequal to exclusive or binary addition. An expression of the form x y is called a conjunction and the operands x and y are called. conjuncts An expression of the form x y is called a disjunction and the operands are called. 1 Basic Theories 4, disjuncts An expression of the form x y is called an implication x is called the antecedent and. y is called the consequent An expression of the form x y is called a reverse implication x is. called the consequent and y is called the antecedent An expression of the form x y is called an. equation x is called the left side and y is called the right side An expression of the form x y is. called an unequation and again the operands are called the left side and the right side. The following truth table shows how the classification of binary expressions formed with two. operand operators can be obtained from the classification of the operands Above the horizontal. line the pair T T means that both operands are theorems the pair T means that the left operand. is a theorem and the right operand is an antitheorem and so on Below the horizontal line T. means that the result is a theorem and means that the result is an antitheorem. Infix operators make some expressions ambiguous For example T T might be read as the. conjunction T which is an antitheorem disjoined with T resulting in a theorem Or it might. be read as conjoined with the disjunction T T resulting in an antitheorem To say which is. meant we can use parentheses either T T or T T To prevent a clutter of. parentheses we employ a table of precedence levels listed on the final page of the book In the. table can be found on level 9 and on level 10 that means in the absence of parentheses. apply before The example T T is therefore a theorem. Each of the operators appears twice in the precedence table The large versions. on level 16 are applied after all other operators Except for precedence the small versions and. large versions of these operators are identical Used with restraint these duplicate operators can. sometimes improve readability by reducing the parenthesis clutter still further But a word of. caution a few well chosen parentheses even if they are unnecessary according to precedence can. help us see structure Judgement is required, There are 256 three operand operators of which we show only one It is called conditional. composition and written if x then y else z fi We call x the if part we call y the then part and. we call z the else part Here is its truth table,T T T T T T T T. if then else fi T T T T, For every natural number n there are 22n operators of n operands but we now have enough. When we stated earlier that a conjunction is an expression of the form x y we were using x y to. stand for all expressions obtained by replacing the variables x and y with arbitrary binary. expressions For example we might replace x with T and replace y with T. to obtain the conjunction T T Replacing a variable with an expression is. called substitution or instantiation With the understanding that variables are there to be replaced. we admit variables into our expressions being careful of the following two points. 5 1 Basic Theories, We sometimes have to insert parentheses around expressions that are replacing variables in. order to maintain the precedence of operators In the example of the preceding paragraph. we replaced a conjunct x with an implication T since conjunction comes. before implication in the precedence table we had to enclose the implication in parentheses. We also replaced a conjunct y with a disjunction T so we had to enclose the. disjunction in parentheses, When the same variable occurs more than once in an expression it must be replaced by the. same expression at each occurrence From x x we can obtain T T but not T. However different variables may be replaced by the same or different expressions From. x y we can obtain both T T and T, As we present other theories we will introduce new binary expressions that make use of the. expressions of those theories and classify the new binary expressions For example when we. present Number Theory we will introduce the number expressions 1 1 and 2 and the binary. expression 1 1 2 and we will classify it as a theorem We never intend to classify a binary. expression as both a theorem and an antitheorem A statement about the world cannot be both true. and in the same sense false a circuit s output cannot be both high and low voltage If by. accident we do classify a binary expression both ways we have made a serious error But it is. perfectly legitimate to leave a binary expression unclassified For example 1 0 5 will be neither a. theorem nor an antitheorem An unclassified binary expression may correspond to a statement. whose truth or falsity we do not know or do not care about or to a circuit whose output we cannot. predict A theory is called consistent if no binary expression is both a theorem and an antitheorem. and inconsistent if some binary expression is both a theorem and an antitheorem A theory is called. complete if every fully instantiated binary expression is either a theorem or an antitheorem and. incomplete if some fully instantiated binary expression is neither a theorem nor an antitheorem. 1 0 0 Axioms and Proof Rules, We present a theory by saying what its expressions are and what its theorems and antitheorems. are The theorems and antitheorems are determined by the five rules of proof We state the rules. first then discuss them after, Axiom Rule If a binary expression is an axiom then it is a theorem If a binary expression is. an antiaxiom then it is an antitheorem, Evaluation Rule If all the binary subexpressions of a binary expression are classified then it is. classified according to the truth tables, Completion Rule If a binary expression contains unclassified binary subexpressions and all ways. of classifying them place it in the same class then it is in that class. Consistency Rule If a classified binary expression contains binary subexpressions and only one. way of classifying them is consistent then they are classified that way. Instance Rule If a binary expression is classified then all its instances have that same. classification,1 Basic Theories 6, An axiom is a binary expression that is stated to be a theorem An antiaxiom is similarly a binary. expression stated to be an antitheorem The only axiom of Binary Theory is T and the only. antiaxiom is So by the Axiom Rule T is a theorem and is an antitheorem As we present. more theories we will give their axioms and antiaxioms they together with the other rules of proof. will determine the new theorems and antitheorems of the new theory. Before the invention of formal logic the word axiom was used for a statement whose truth was. supposed to be obvious In modern mathematics an axiom is part of the design and presentation of. a theory Different axioms may yield different theories and different theories may have different. applications When we design a theory we can choose any axioms we like but a bad choice can. result in a theory with no applications, The entry in the top left corner of the truth table for the two operand operators does not say. T T T It says that the conjunction of any two theorems is a theorem To prove that T T T. is a theorem requires the binary axiom to prove that T is a theorem the first entry on the row. of the truth table to prove that T T is a theorem and the first entry on the row of the truth. table to prove that T T T is a theorem,The binary expression. contains an unclassified binary subexpression so we cannot use the Evaluation Rule to tell us. which class it is in If x were a theorem the Evaluation Rule would say that the whole expression. is a theorem If x were an antitheorem the Evaluation Rule would again say that the whole. expression is a theorem We can therefore conclude by the Completion Rule that the whole. expression is indeed a theorem The Completion Rule also says that. is a theorem and when we come to Number Theory that. 1 0 5 1 0 5, is a theorem We do not need to know that a subexpression is unclassified to use the Completion. Rule If we are ignorant of the classification of a subexpression and we suppose it to be. unclassified any conclusion we come to by the use of the Completion Rule will still be correct. In a classified binary expression if it would be inconsistent to place a binary subexpression in one. class then the Consistency Rule says it is in the other class For example suppose we know that. expression0 is a theorem and that expression0 expression1 is also a theorem Can we. determine what class expression1 is in If expression1 were an antitheorem then by the. Evaluation Rule expression0 expression1 would be an antitheorem and that would be. inconsistent So by the Consistency Rule expression1 is a theorem This use of the Consistency. Rule is traditionally called detachment or modus ponens As another example if. expression is a theorem then the Consistency Rule says that expression is an antitheorem. Thanks to the negation operator and the Consistency Rule we never need to talk about antiaxioms. and antitheorems Instead of saying that expression is an antiaxiom or antitheorem we can say. that expression is an axiom or theorem But a word of caution if a theory is incomplete it is. possible that neither expression nor expression is a theorem Thus antitheorem is not the. same as not a theorem Our preference for theorems over antitheorems encourages some. shortcuts of speech We sometimes state a binary expression such as 1 1 2 without saying. anything about it when we do so we mean that it is a theorem We sometimes say we will prove a. binary expression meaning we will prove it is a theorem. End of Axioms and Proof Rules,7 1 Basic Theories, We now replace the binary antiaxiom with an axiom With our two binary axioms and. five proof rules we can now prove theorems Some theorems are useful enough to be given a name. and be memorized or at least be kept in a handy list Such a theorem is called a law Some laws of. Binary Theory are listed at the back of the book Laws concerning have not been included but. any law that uses can be easily rearranged into one using All of them can be proven using. the Completion Rule classifying the variables in all possible ways and evaluating each way When. the number of variables is more than about 2 this kind of proof is quite inefficient It is much. better to prove new laws by making use of already proven old laws In the next three subsections. we see how,1 0 1 Expression and Proof Format, The precedence table on the final page of this book tells how to parse an expression in the absence. of parentheses To help the eye group the symbols properly it is a good idea to leave space for. absent parentheses Consider the following two ways of spacing the same expression. According to our rules of precedence the parentheses belong around a b so the first spacing is. helpful and the second misleading, An expression that is too long to fit on one line must be broken into parts There are several. reasonable ways to do it here is one suggestion A long expression in parentheses can be broken. at its main connective which is placed under the opening parenthesis For example. first part,second part, A long expression without parentheses can be broken at its main connective which is placed under. where the opening parenthesis belongs For example,first part. second part, Attention to format makes a big difference in our ability to understand a complex expression. A proof is a binary expression that is clearly a theorem What is clear to one person may not be. clear to another so a proof is written for an intended reader One form of proof is a continuing. equation with hints,expression0 hint 0,expression1 hint 1. expression2 hint 2,expression3, This continuing equation is a short way of writing the longer binary expression. expression0 expression1,expression1 expression2,expression2 expression3. The hints on the right side of the page are used when necessary to help make it clear that this. continuing equation is a theorem The best kind of hint is the name of a law The hint 0 is. supposed to make it clear that expression0 expression1 is a theorem The hint 1 is supposed. to make it clear that expression1 expression2 is a theorem And so on By the transitivity of. this proof proves the theorem expression0 expression3 A formal proof is a proof in which. every step fits the form of the law given as hint The advantage of making a proof formal is that. each step can be checked by a computer and its validity is not a matter of opinion. 1 Basic Theories 8, Here is an example Suppose we want to prove the first Law of Portation. a b c a b c, using only previous laws in the list at the back of this book Here is a proof. a b c Material Implication,a b c Duality,a b c Material Implication. a b c Material Implication, From the first line of the proof we are told to use Material Implication which is the first of the. Laws of Inclusion to obtain the second line of the proof The first two lines together. a b c a b c, fit the form of the Law of Material Implication which is. because a b in the proof fits where a is in the law and c in the proof fits where b is in the. law The next hint is Duality and we see that the next line is obtained by replacing a b. with a b in accordance with the first of the Duality Laws By not using parentheses on that. line we silently use the Associative Law of disjunction in preparation for the next step The next. hint is again Material Implication this time it is used in the opposite direction to replace the. first disjunction with an implication And once more Material Implication is used to replace the. remaining disjunction with an implication Therefore by transitivity of we conclude that the. first Law of Portation is a theorem,Here is the proof again in a different form. a b c a b c Material Implication 3 times,a b c a b c Duality. a b c a b c Reflexivity of, The final line is a theorem hence each of the other lines is a theorem and in particular the first line. is a theorem This form of proof has some advantages over the earlier form First it makes proof. the same as simplification to T Second although any proof in the first form can be written in the. second form the reverse is not true For example the proof. a b a b a Associative Law for,a b a b a a Law of Inclusion. cannot be converted to the other form And finally the second form simplification to T can be. used for theorems that are not equations the main operator of the binary expression can be. anything including or, The proofs in this book are intended to be read by people rather than by a computer Sometimes it. is clear enough how to get from one line to the next without a hint and in that case no hint will be. given Hints are optional to be used whenever they are helpful Sometimes a hint is too long to fit. on the remainder of a line We may have,expression0 short hint. expression1 and now a very long hint written just as this is written. on as many lines as necessary followed by,expression2. We cannot excuse an inadequate hint by the limited space on one line.

B. Sc. Honours (Statistics) 6 SEMESTER V STAT?C?501 Stochastic Processes and Queuing Theory Core Discipline 4 Practical/Lab. Work 2 STAT?C?502 Statistical Computing Using C/C++ Programming

1 Shivaji University, Kolhapur B. Sc. III Statistics Structure of the course To be implemented from June 2010 (i) Theory Sr. No. Title of the paper Paper No. Total Mark 1 Probability Distributions V 100 2 Statistical Inference VI 100 3 Designs of experiment and Sampling Methods VII 100 4 Programming in C and Operations Research VIII 100 (ii) Practical Distribution of Marks of Practical Papers ...

Such people must prepare for entrance exams like GATE/PGCET etc. To face these exams one must prepare from 3rd year itself. Most of the syllabus in GATE includes only 2nd year and 3rd year core subjects. Related Exams: GATE: Conducted by one of seven Indian Institutes of Technology in rotation, Graduate Aptitude Test in Engineering (GATE) is an annual exam for admission to M.Tech and M.S ...

S122 SERIES Hand-Held Fusion Splicer With its super low pro? le and new user interface, the FITEL S122 series fusion splicer offers next generation workability for every splicing ? eld, FTTX, LAN, backbone, or long-haul installations. Combining the portability, power ? exibility and ? eld rug-

II Swarnim Raghav Vidya Bharati School III Vansh Saxena Sunrise Play School . III Atharv Bhandula Vidya Bharati School 4 Fashion Show 3+ I Shnaya Raghav Vidya Bharati School II Nivika Arora Decorum play and Nursery School II Tejasvini Bachpan A play School III Dhupita Shami Champs Valley Consolati on Samriddhi Sunrise Play School 5 Fancy Dress ...

1 Introduction High energy physics experiments study properties of el-ementary particles. Accelerator based experiments can currently produce particle energies up to a few TeV while cosmic rays were found up to 1021eV. The data aquisition system (DAQ) of a physics ex-periement captures the data generated by a detector. A DAQ system simulation model includes a number of distinct components ...

1. INTRODUCTION 1.1 Background The adoption of digital design and manufacturing technology and BIM technologies in construction have opened up new opportunities for architects who are willing to adapt towards integrated processes to assume leadership roles in the creation of the built environment (Bedrick, 2006). Architects have

Education Service "God blew and they were scattered" Did God really help the English defeat the Spanish Armada? This resource was produced using documents from the ...