Home

Brock_Das_Tuhin_2012

1. we can conclude u q CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 3l PBC In this case we have a derivation I 2V L Now assuming u be a valuation u E T holds If u V we can conclude u E L from the induction hypothesis But this is a contradiction So we conclude u V Induction To prove the soundness of the induction rule we will have to show that IF T E e 0 a D v E glx 1 z and D o E vx 1 z then the following holds rEg Proof Let us assume u mz f for all 8 We have to show that u mz q We distinguish three cases If u x 0 then we have u mz p since u ma p 0 x by the first assumption Now let us assume u x gt 0 and define u by u y u y for y x and u x u x 1 Then u mz p if u mz y x 1 x By the sec ond assumption the latter is implied by u mz q and u mz 8 for all 8 T We iterate the previous argument u x times so that we finally can apply the first assumption The case u x 0 is shown analogously An Inference rule for reasoning about program is sound when validity of it s premises implies the validity of it s conclusion Skip To prove the soundness of the skip rule we will have to show that If P E p V then the following holds T p skip v Proof Let us assume u mz p for all o P We have to show that u mz p skip V By the induction we
2. 47 Application of the ForallRight rule 48 Application of the ExistsLeft rule 48 Application of the ExistsRight rule 49 vil 5 1 5 2 5 3 5 4 5 9 6 1 6 2 6 3 6 4 6 5 6 6 6 7 6 8 6 9 6 10 6 11 6 12 6 13 Class diagram of Formula 53 mas de a eam a ek es 53 Relationship between Formula and Term 53 Class diagram of Program 119 5 ra Go ats aes Gare i Tabu 54 Class diagram of Term ua exu Ye ua ee keh an le eB 54 Relationship between Formula and Program 54 The user interface of this system o a 56 The current goal is displayed in the Assertions window 56 The assumption of the current proof is displayed in the Assumptions onse A e ee we ee ee es eee a ee ee a Ge RS A 57 Activation of a left hand rule AndLeft 57 The left hand rule AndLeft has been applied 58 Selection of formula in Assertions window 59 Application of derivation button in Assertions window 59 Application of an axiom rule 00 eee eee 60 Mapping of variable a to i in unifier 444i sei ee a 60 Mapping of variable a to rin unifier e 4c uat Roo RR RR 61 Application of unification 2 81 9 sn ete EIER RU 62 The completion of the main proof llle 62 Maximized view of Proof Explorer window 63 Chapter 1 Introduction Dynamic Logic is a formal
3. Proof of 2nd step CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 9 e I r i i n r i m i n A i n gt r i m A i lt n gt r m i m m Ai 1 lt n gt r m i 1 m A i 1 lt n I r m i 1 Proof of 3rd step e I r i i lt n z r i m A i n A i gt n gt r i m A i n gt r n m We can see DL as a generalization of Hoare logic In terms of expressiveness dynamic logic is more powerful than Hoare logic because in addition to partial correctness program termination and program implication can also be expressed in DL Let us consider the following DL formula 4 10 15 e laly where y and w are first order formulas This formula has the same meaning as the Hoare triple e o v given a is executed in a state satisfying v if the program a terminates the final state will satisfy v 2 3 First order dynamic logic In this section we are going to explore a specific version of dynamic logic namely first order dynamic logic This version of dynamic logic will be used as the logical basis of our deductive system 2 3 1 Syntax The language of first order Dynamic Logic is built upon classical first order logic A set of programs and a set of formulas are defined on top of a vocabulary of function symbols and predicate symbols 7 These two sets use the modal construct for interacting with each other Programs and formulas in DL are usually defined b
4. 17 Eric C R Hehner Specifications Programs and Total Correctness Accessed 30th August 2012 http www cs toronto edu hehner SPTC pdf 18 Wikipedia Loop invariant Accessed 30th August 2012 http en wikipedia org wiki Loop_invariant 19 Gerwin Klein JFlex User s Manual Accessed 30th August 2012 http jflex de manual html 20 UML basics The class diagram Accessed 30th August 2012 http www ibm com developerworks rational library content RationalEdge sep04 bell 21 The KeY Project Accessed 30th August 2012 http www key project org BIBLIOGRAPHY 70 22 23 24 Sanan 25 26 Wikipedia First order logic Accessed 30th August 2012 http en wikipedia org wiki First order logic Completeness incompleteness and what it all means first versus second order logic Accessed 30th August 2012 http lesswrong com 1w 93q completeness incompleteness and what it all means Collatz conjecture Accessed 30th August http en wikipedia org wiki Collatz conjecture ESC Java2 Summary Accessed 30th August http kindsoftware com products opensource ESCJava2 Boogie An Intermediate Verification Language Accessed 30th August http research microsoft com en us projects boogie
5. Term Atomic Formulas and Programs In all versions of DL formulas that take the form r t t2 t where r is an n ary predicate symbol of gt gt and t4 t2 tn are terms of gt gt are called atomic formulas of the first order vocabulary In this deductive system a predicate symbol can be any of the following constructs lt gt gt So example of an atomic formula can take the form of a b or a b gt c d where a b c d Term Various programming constructs are used for defining programs inductively from atomic programs Selection of different classes of atomic programs and program ming constructs will result in different classes of programs Giving meaning to a compound program requires to give meanings to its constituent parts If x X and t is a term of 7 an atomic program can be defined as a simple assignment x t Tests Originally in DL conversion of a formula into program requires a test operator 7 For our version of implementation we will allow only quantifier free first order formulas as tests This version of test is called poor test Another version of tests CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 11 called as rich test does not place any restrictions on the form of tests and allows any DL formulas So using rich tests a formula can contain other programs which could be other tests which makes it impractical to implement In the poor test version we can d
6. mz b gt p1 V b gt p2 V The latter is equivalent to 1 y mz b gt p1 V 2 y mz b gt p2 V Now let us distinguish two cases If y mz b then y mz pl V This im plies that for all v with y v mz pl we have v mz W We can conclude y v mz if b then pl else p2 fi so that u mx p if b then pl else p2 fi V follows The case y mz b i e y mz b is shown analogously Loop To prove the soundness of the loop rule we will have to show that IF T E p e T gy Ab E pl y and Ir Aa b gt Y then the following holds T p while b do pl od V Proof Suppose u mz B for all 8 T and v is a valuation so that u v mz p If there is an n gt 0 and vp Un with v vo and v mz b forO lt i lt n and v vj41 mz pl and v mz b then we have to show that v mz v In order to do so we have to show by induction on i lt n that v mz q For i 0 this is trivial since vp v and our first assumption I p y In the induction step CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 33 we have v mz b and by the induction hypothesis v mz p From the second assumption we get v 4 1 mz q because vi vjj1 mz pi finishing the induction This shows v mz y so that v mz y b follows The third assumption shows v mz v 3 9 Incompleteness of this
7. AL In this case I I 1 pz and we have a derivation I p1 pz F V Now assuming u be a valuation u I and u E y 2 holds From the definition of we get u H p1 pa iff u H py and u E v Which implies u Iu y and u i holds By the induction hypothesis we can conclude u V and hence I 4 Pa E V VL In this case T I p V 2 and we have derivations I y V and T p2 F V Now assuming u be a valuation u E I and u E q V 2 holds From the definition of we get u y or u E v In the first case we conclude satis fies I y Using induction hypothesis we conclude u V CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 30 gt L In this case T I y gt v and we have derivations I Fy and I q E V Now assuming u be a valuation u I and u y1 gt q holds From the definition of we get u p1 gt y2 iff u E s oru E qi amp L In this case I I p 3 and we have derivations I 1 Pa pa gt qi E V Now assuming u be a valuation u T and u v1 2 holds From the defini tion of we get u H y1 pa iff u y1 gt yo and u E p2 gt qv AL In this case T I p and we have a derivation ty Now assuming u be a valuation u I and u g holds and by induction hypothesis we get u y As this is a contradiction no
8. m z u u malo glp v u u mz p and u mz v z o V v u u ma p or u mz v z o gt v 2 u if u mz p then u mz y alg 1 u if u mz y then u mz v and vice versa z Vx o F u Va Z u a x mz y e mz 3x p u da Z u a x mz p e mz o p u Vv if u v mz o then v mz y 2 3 3 Satisfiability and Validity of Formulas Let Z be the model of integer numbers and u be a state in S Now for a formula y eu p if u mz y e ifu H for all u S7 e p y if for a valuation u S the property u E for all 8 T implies u CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 18 2 4 Reasoning in FODL Reasoning in first order dynamic logic can be performed in two ways uninterpreted reasoning and interpreted reasoning Reasoning in the uninterpreted level deals with the properties that can be expressed in the logic that are independent of the domain of interpretation In contrast reasoning in the interpreted level involves the use of the logic which depends on a particular domain or a limited class of domains In this level syntactically programs and formulas are the same as on the uninterpreted level except the assumption of a fixed model or class of models Properties of particular models over which programs are interpreted determine the computational behavior
9. 4 5 4 6 4 7 4 8 4 9 4 10 4 11 4 12 4 13 4 14 4 15 4 16 4 17 4 18 4 19 4 20 4 21 4 22 4 23 4 24 4 25 4 26 Comparison of values of i and r in the given example 8 Example of Valid and Invalid formulas 36 A valid formula is entered ea da Baad pum IERI P IN Rer d 36 After application of the implication rule 36 User is asked to enter the loop invariant 37 While rule has been applied o oaaao 37 List of axioms is loaded oie RR EGRE Ss 38 Application of user selected axiom a a 38 A portion of the proof is d estee o ems 38 A completed proof x 4 032 2m acho ee oe ie ia RU ee eee E Bas 39 Application of the AndLeft rule 40 Application of the AndRight rule 40 Application of the OrLeft rule lll 41 Application of the OrRight rule 41 Application of the ImpLeft rule 42 Application of the ImpRight rule 42 Application of the Induction rule 43 Application of the NotLeft rule 43 Application of the NotRight rule len 44 Application of the PBC rule atu uet Io ok o Se x Re 44 Application of the Assignment rule 0 45 Application of the if else rule 2l lens 45 Application of the loop rule 34 e RO Ser a Sede deo Dent 46 Application of the ForallLeft rule
10. CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 29 I Let us consider the case of a finite subset of the set of integer numbers i e a model ai an In this case an existential formula 4x q is true if it is true for one of the integer elements a4 dn Assuming the terms f tn denote the elements i e U t a dx q is true if o ti x V V q t x is true As a re sult we get a rule similiar to V elimination The formula y must be independent of x and x be local to that subtree motivating the variable condition of this rule JE Let us consider the case of a finite subset of integer numbers i e a model lai Gn In this case an existential formula 3x is true if it is true for one of the integer elements a a4 Assuming the terms t tn denote the elements i e U t a dx p is true if plt x V V yltn x is true As a result we get a rule similiar to V elimination The formula x must be independent of x and x be local to that subtree motivating the variable condition of this rule ive dep x JE a ib L By the induction hypothesis we have T t t and IT W t x Let u be a valuation so that u mz f for all 8 T Then u tj u t3 and u mz Vlt x From the Lemma 3 1 4 we obtain ulu t x mz WV This im plies u u t3 x mz W and hence u mz V t x using the Lemma 3 1 4 again
11. R A Struth G Eds Relations and Kleene Algebra in Computer Science 50 54 University of Sheffield CS 06 09 2006 Laura Kovacs Andrei Voronkov Finding Loop Invariants for Programs over Arrays Using a Theorem Prover FASE 09 Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering Held as Part of the Joint European Conferences on Theory and Practice of Software Pages 470 485 2009 68 BIBLIOGRAPHY 69 10 Benjamin Weib Deductive Verification of Object Oriented Software KIV Sci entific Publishing 2010 11 Wikipedia Modal Logic Accessed 30th August 2012 http en wikipedia org wiki Modal logic 12 Garson James Modal Logic The Stanford Encyclopedia of Philosophy Win ter 2009 Edition Edward N Zalta ed Accessed 30th August 2012 http plato stanford edu entries logic modal 13 Wikipedia Dynamic logic modal logic Accessed 30th August 2012 http en wikipedia org wiki Dynamic logic modal logic 14 Eric C R Hehner University of Toronto Specifications Programs and Total Correctness Accessed 30th August 2012 http www pm inf ethz ch education seminars se presentations Presentation Eigenmann pdf 15 Wikipedia Hoare logic Accessed 30th August 2012 http en wikipedia org wiki Hoare logic 16 Partial and total correctness Accessed 30th August 2012 http www ida liu se TDDA43 slides ax sem tot corr pdf
12. immediately CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 25 Left logical rules Right logical rules Ionen rot Hip nena L Tha AR Tava V L mou R P AE VR Toate OL oo oR ESTAS OF eae AE LEY oL ned rera VL Prop VR If no free occurrence of a in any formulas of I If no free occurrence of a in any formulas of I and in V gt PBC ih ify erT Table 3 3 Logical rules for first order reasoning If the case y is one of the following formulas true false p1 Y1 A Pa Y1 V 9 or Y gt 2 then the proof is the straight forward applications of the induction hy pothesis Now let us assume y Qx y where Q V 3 l The free variables of y in cludes the free variables of y and the variable x Consequently the valuations u a x CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 26 T p w DF p skip V skip P assignment PE p 5 p1 W A 5 p2 V TF p if b then pl else p2 fiw if else TE pip TjondE pljp TF p gt Y TF swhilebdoplodW loop Table 3 4 Inference rules for dynamic reasoning and v a x for an arbitrary a Z coincide on all free variables in v So we can conclude uk e gt u a x y for all some a Z v a x H v for all some a Z e vb Here the second equivalence is an application of the induction hypothesis Finally let us assume y a y Now free
13. 0 while i lt n dor r m i i 1 0d Jr n m amp f r oi 0j r i mandi n EP r 0j r 0 mando n S P 0 0 mando lt n 0 0 m gt MA 0 n Br i mandi lt nandi lt n gt r r mji i 1 r i mandi lt n A r i mandi lt nandnot lt n gt r 2 n m yi a a 0 gt Assumptions gt S 4 Theorems gt a NISUS 3 rozv ome Ce AE h F oeR ramon a gt banda lt b lt gt a b mu File View Tools Help D gc dH O O while i lt n do r r m i 1 od r n m i lt n dor r mji i l od r 2 n m Gr i mandi lt nandi lt n gt r r mji 1 1 r i mandi lt n 8 r i mandi enandnot lt n gt r n m Caer onet ome NotLeft NotRight E RelAPS Default Workspace File View Tools Help D gc MB r imandi e nandi n gt r r mji i 1 r e i mandi lt n KB r i mandi e nandnot lt n gt r n m El ImpLeft __ImpRight Figure 4 8 A portion of the proof is done Finally when the proof is done for an entered formula a completed proof is shown with a larger sized tick mark in front of the root of the tree in the proof explorer window This feature confirms the user about the completion of the proof An example of a completed proof is illustrated in Figure 4 9 CHAPTER 4 OVERVIEW OF THE SYSTEM 39 Gif n gt 0 gt r Oi
14. Application of the OrRight rule CHAPTER 4 OVERVIEW OF THE SYSTEM 42 dit pe Meme Proofs a acbs becs acc asc Adal AA LXI F Proofs cQ acbs b cs acc Figure 4 14 Application of the ImpLeft rule ld ge E I me DE a lt bmb lt cma lt c Proofs Pacbe gt becerace D Q acbz b cz a c Qbecs nec A Figure 4 15 Application of the ImpRight rule CHAPTER 4 OVERVIEW OF THE SYSTEM 43 ASA x y l1 z Figure 4 16 Application of the Induction rule ud pt Marne E Prosts SY not a b 5 a bORa s b Q a boRa b Hie View Tools Help Qu dit pe ome FE Proof S X not a b gt a bORa sb S Barboma d a lt b Figure 4 17 Application of the NotLeft rule CHAPTER 4 OVERVIEW OF THE SYSTEM 44 id pt pn Mme Hy e not a lt b Qu Figure 4 18 Application of the NotRight rule dd eU pe Mme Is Proci G xay 9 Cle not x y z Figure 4 19 Application of the PBC rule CHAPTER 4 OVERVIEW OF THE SYSTEM 45 oe Ir 0 r O m and 0 lt n r r r 0 mando lt n i m andi cen andi n m ly m remi miei r mandi en ra lmandi en adnot lt n e r n n 9 Clk 0 O m and 0 lt n E id et pn mame E Proets c X npn 0 w gt rs 03 Gow
15. In the following step applying a proof rule in the resultant derivation will generate a new derivation 3 F V3 If we apply the proof rule continuously finally we will get the conclusion I V The resulting derivation is actually a tree where assumptions are represnted as leaves applications of rules are represented as intermediate nodes and the conclusion is represented as the root of the tree The inference rules of our deductive system are listed below The sequencing and consequence rules of Hoare logic are implicitly incorporated in the loop rule of our calculus In this system equational reasoning is handled in a special way in order to make the reasoning close to the actual human reasoning Users of this system have the privilege to choose a particular axiomatic rule from a list of applicable rules to ini tiate the process of equational reasoning This feature is implemented in a way so that one will experience the flavor of doing the equational reasoning with a pen and a piece of paper An example of equational reasoning is demonstrated in Chapter 4 As we mentioned earlier the implemented inference rules for reasoning about pro grams are equivalent to Hoare logic rules and the structure of these rules is very close to the actual Hoare logic rules which makes it very simple to understand the techniques of program property verification The combination of these features of DL rules FOL rules and equational reasoning make this sys
16. example let us consider the Hoare triple n gt 0 p r n where p is a program In this example if the precondition n gt 0 is true before the execution of the program p and if p terminates then we will be ended up in a state where the postcondition r n is satisfied Six rules of Hoare logic that are used for program property verification are given below e Skip o skip y Assignment v a x x a v where v a x denotes the substitution of a for x e Cot x b3oitvi ieJCo Cilv e bjCotv Leo Cid oif bthen Co else Cy fi p LonbiC v Loop OIE e Sequencing e Conditional eoe p JO v 29 e C y e Consequence Rules are written with premises above a horizontal line and the conclusions below it If some conditions need to be satisfied for the application of the rule it is writ ten by its side In a formal proof system a collection of rules is used to carry out stepwise deductions If the number of premises in a rule is zero it is called an ax iom A derivation using these rules generates a proof tree which consists of nodes that represents the instances of applied rules Leaves of a proof tree represent either the instances of axioms of the system or unfinished sequents whose derivations are not finished yet Therefore a derivation tree for a derivable sequent will not have any unfinished leaves and such a derivation tree can be called finished For a derived rule a de
17. future improvements include the production of Latex output of the proofs which will give the user the flexibility of exporting their work in the form of latex code In that case a researcher could use the system to prove the correctness of a program and could use the generated Latex output for publications Bibliography 1 E Aameri B Winter M A First Order Calculus for Allegories In de Swart H Eds Relational and Algebraic Methods in Computer Science RAMIiCS 12 Lecture Notes in Computer Science 6663 74 91 2011 Edsger W Dijkstra Guarded commands nondeterminacy and formal derivation of program Communications of the ACM Volume 18 Issue 8 August 1975 Winfried Karl Grassmann Jean Paul Tremblay Logic and Discrete Mathemat ics Prentice Hall ISBN 10 0135012066 ISBN 13 978 0135012062 Edition 1 Dec 28 1995 R Hahnle M Heisel W Reif W Stephan An interactive verification system based on dynamic logic In Proceedings of CADE 306 315 1986 David Harel Dexter Kozen Jerzy Tiuryn Dynamic Logic The MIT Press 2000 M Heisel W Reif W Stephan Program verification using dynamic logic Lec ture Notes in Computer Science Springerlink Volume 329 1988 102 117 1988 M Huth M Ryan Logic in Computer Science Modelling and reasoning about systems Cambridge University Press 2nd Edition 2004 Glanfield J Winter M RelAPS A Proof System for Relational Categories In Schmidt
18. have I E p V i e we have u mz p V By the defini tion of mz this implies that we have for all v that if u v mz p then v mz W Since mz skip u u u is a valuation we can get mz p mz p skip so that we have if u v mz p skip then v mz W for all v i e u mz p skip V Assignment To prove the soundness of the assignment rule we will have to show that I T E p V a x then the following holds CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 32 T p x a Y Proof Let us assume u mz q for all o I We have to show that u mx p x a V By induction we have D E p V a x i e u mz p V a x By definition of mz this implies that for all v if u v mz p then v mz V a x This is equivalent to v a x mz W Now since mz x a v v x a v is a val uation we get v mz x a V and hence u mz p x a V If else To prove the soundness of the if else rule we will have to show that If E p b gt pl V A b p2 V then the following holds T p if b then pl else p2 fi V Proof Let us assume u mz q for all o I We have to show that u mx p if b then pl else p2 fi V By induction we have T E p b gt p1 V 2b p2 W So u mz p b gt p1 V b gt p2 V By definition of mz we have for all y that if uy mz p then y
19. the user to select a mapping of the unmapped variables As we can see from Figure 6 9 for the application of the axiom rule a b gt a gt b and CHAPTER 6 USER MANUAL 59 Figure 6 6 Selection of formula in Assertions window Figure 6 7 Application of derivation button in Assertions window a lt b to the selected variable n of formula r n m variable b in the left hand side of the rule is automatically mapped to the selected variable n So to map the other variable i e a in the left hand side of the rule the user of this system will have to either select a term from the list or enter a new term Now the selection of a term CHAPTER 6 USER MANUAL 60 from the list of available terms i for mapping of the variable a will result in Figure 6 10 Figure 6 8 Application of an axiom rule LITT LI Quem eti conemdi n or ctm EL fame Figure 6 9 Mapping of variable a to i in unifier CHAPTER 6 USER MANUAL 61 Figure 6 10 Mapping of variable a to i in unifier The application of unifier is shown in Figure 6 11 As we can see the atomic formula r n m has been converted to r i m and for making it possible two assumptions will be added to the current proof as we will see in Figure 6 12 Now if we click on derivation button of the Working Area window we will have r i m in the Assertions window and two new formulas i gt 0 and i lt 0 will be added und
20. 1 lt i lt n States as Valuations Values of program variables determine all relevant information at any moment during the computation Therefore states are represented by valuations u v etc of the variables V over the carrier of the model Z As we have used the set of integers as the model of this system all valuations in this system map a variable to an integer number So all formulas of this system are interpreted over the set of integers and CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 15 all program variables store integer numbers We denote the set of all valuations or states over the model Z by S Assuming u as the beginning valuation after the execution of the program a if we halt in a valuation v then we can associate the pair u v of such valuations with the program a In this case u v will be referred as an input output pair of a and will be written as u v mz a As we mentioned in this system a valuation maps a set of program variables to a set of integer numbers So a set of integer numbers is used here to represent each element of the input output pair of a program a for finding the value of a term and for evaluating the truth value of a formula Let us consider a formula as an example x 0 y 2 gt x x y y x y z y x A general input output pair for the program of the given formula can be given as u ulu z u y z ufur u y 2 2 ululo u y 2 y yl mala where ulu z u y z ufur u
21. An Interactive Theorem Prover for First Order Dynamic Logic Tuhin Kanti Das Department of Computer Science Supervisor Professor Michael Winter Submitted in partial fulfillment of the requirements for the degree of Master of Science Faculty of Mathematics and Science Brock University 5t Catharines Ontario Qu Kanti Das 2012 To Professor Michael Winter amp My Parents Abstract Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs The method of proving correctness of properties of a computer program using the well known Hoare Logic can be implemented by utilizing the ro bustness of dynamic logic For a very broad range of languages and applications in program verification a theorem prover named KIV Karlsruhe Interactive Verifier Theorem Prover has already been developed But a high degree of automation and its complexity make it difficult to use it for educational purposes My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria As the key purpose of this system is to serve as an educational tool it is a self explanatory system that explains every step of creating a derivation i e proving a theorem This deductive system is implemented in the platform independent programming language Java In addition a very popular combination of a lexical analyzer generator JF
22. But this feature makes this system incomplete To make this system complete the rule for the total correctness assertion must have to be implemented The other reason for which this system is incomplete is the choice of the implicit model namely the set of the integer numbers which is incomplete Godel s incom pleteness theorem states that any effective first order theories which include a suffi CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 34 cient portion of the theory of the natural numbers can never be both consistent and complete This is a theorem about an arithmetic structure where the implicit model is the natural numbers According to this theorem any arithmetic that can model these natural numbers suffers from the problem of incompleteness 22 23 As we have used a first order arithmetic model the set of integer numbers it is not possible to have completeness in this deductive system One possible solution to this problem could be the use of the set of real numbers as the implicit model instead of the set of integer numbers But as we mentioned above due to the absence of a rule for the total correctness assertion it would not be possible for this system to be complete even if we use any model which is complete Chapter 4 Overview of the System In the first section of this chapter we will discuss the effectiveness of this system as an educational tool To derive every step of a proof in this system the user will hav
23. In this system we have considered only one model the set of integer numbers Z to give semantics to the syntactic constructs of the system In this model integer variables are the elements of the set of variables and integer numbers are used as con stant values In addition in this system the meaning of each of the predicate symbols or function symbols is fixed The usual interpretation of arithmetic operators and relational operators lt gt gt is used here to give meaning to a function or a predicate symbol So for example the binary function symbol is interpreted by adding two integer numbers and the value it returns is also an integer number In this thesis we will be using the notation Z to denote the standard model based on the set of integers Z i e Z Z and mz for giving meaning to the syntactic constructs of this system over the model of the set of integer numbers Z Definition 3 Let us consider Z the model of integer numbers A valuation u V gt Z is a function from the set of variables V to the universe of the model For a valuation u a variable x and a value a Z the valuation denoted by u a z is defined by ula ax def D a rna m iff Ay where yin V Definition 4 Let us consider Z be the model of integer numbers and u be a valua tion The extension u Term gt Z is defined by e u x u x for every x V e uff uiu m Ult ut where t Term for
24. O while i lt n dor remi i 1jod r n m E Y r 2 0 i O while i n dor r m i i 1j0d r 2 n m E Y r 0 i 2 0 r i mandi 2n E Y r20 r 0 mand0 lt n B 0 0 mand0 lt n e Y 0 0 m in Y O lt n B r i mandi lt nandi n gt r r mji i 1 r i mandi lt n E w r r mji i 1 r i mandi 2n B w r r m r 1 mandit i lt n E Y rtm 1 mandi 1 lt n B rm 1 1 mandi 1 lt n E Y rtm i 1 mandi i lt n Y rtm i 1 m v iti lt n wr n E Y r n m r n m wv i n Y i lt n Figure 4 9 A completed proof 4 2 Demonstration of the inference rules In this section we demonstrate the use of each of the inference rules separately with the help of screenshots CHAPTER 4 OVERVIEW OF THE SYSTEM 40 EF ld pt Moone Proof c acbandbecs acc oe acc Pace Figure 4 10 Application of the AndLeft rule 3 dit pn mame ES proc S asbs 105225 Gand bs 4 F a 6andb Ej diet mamar FE Proots S athe 105 a7 6andbs4 S Pancanddas ae bes Figure 4 11 Application of the AndRight rule CHAPTER 4 OVERVIEW OF THE SYSTEM A EF ld et Mme Proofs S Pacbonb lt carced c d ddr 90 m a lt b0Ra lt cm a lt d Proods Pacbonaccera lt d File View Toots Help 2i du ld jt Mame 5 Proofs S X acbORa cs acd Figure 4 13
25. PLEMENTATION 54 AssignStatement IfStatement WhileStatement Figure 5 3 Class diagram of Program mLeft Term mRight Term minfo Opinfo Figure 5 4 Class diagram of Term object can have any number of programs within it while a Program object can also have any number of formulas within it In our system quantifier free formulas are used as test condition which is also referred to as Poor Test Figure 5 5 Poor Test Formula Program Figure 5 5 Relationship between Formula and Program Chapter 6 User Manual The formulas that can be accepted in this system are defined in Section 2 3 During the proof of a derivation the users of this system can apply any of the rules mentioned in Section 3 1 As shown in Figure 6 1 a set of buttons have been added to the appli cation interface for this purpose The buttons are used to apply any of the derivation rules we mentioned in Section 3 1 on the current proof All derivation buttons are disabled by default except PBC and Apply Induction buttons The buttons corre spond to the right hand rules of first order reasoning are enabled based on a subtree that has been selected in the Proof Explorer window An appropriate button for left hand rule of first order reasoning will be enabled if a user of this system selects an assumption in the Assumptions window The buttons related to program reasoning will be activated if the formula of the currect proof has a p
26. Proofs oD edstuicksd o ys xz x z 2 dit pe me E Proofs S Q mts rd yoo amp Prez Figure 4 25 Application of the ExistsLeft rule CHAPTER 4 OVERVIEW OF THE SYSTEM 49 2 amp exists x xeley Figure 4 26 Application of the ExistsRight rule Chapter 5 Implementation In this chapter we will briefly discuss the methods of implementing the system The class hierarchies and relationship between some important classes will also be discussed here 5 1 Brief explanation of source code This deductive system for FODL has been implemented in the platform independent programming language Java using the Netbeans Interactive Development Environ ment Precisely Version 1 7 0 of the Java Development Kit and Version 7 1 1 of NetBeans IDE were used As the set of first order formulas is a subset of the set of dynamic logic formulas one part of this system required us to implement the rules of classical first order logic But Bahar Aameri has already developed those rules of first order logic in her MSc Thesis 1 RelAPS is an interactive system developed by J Glanfield which can be used to perform a relation algebraic proof similar to doing it using pencil and paper 8 Bahar extended this system to full first order logic So we have reused her code with some modification to adapt with our system But as the main part of our work involves the implementation of the rules of Hoare logic for the re
27. Table 3 2 Axiomatic rules for integer numbers Va a a 0 Va axl a Va ax0 0 Va Vb a b b a Va Vb axb bxa Va Vb Vc a b c a b c Va Vb Ve ax bxc axb c Va Vb Vc ax b c axb axc Va Vb Vc a4 b c axc bxc Continued on next page CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 24 Table 3 2 continued from previous page Va Vb Vc ax b c axb axc Va Vb Vc a b c axc bc Va Vb a b b c Ha c Va Vb a b lt b c a lt c Va Vb a b gt b c a gt c Va Vb a lt be b gt a Va Vb a gt b 1 4 a gt b Va Vb a gt b a lt b1 a b Va Vb a gt b a b Va Vb a lt b a gt b Lemma 3 1 1 If the valuations u and v coincide on all variables of t where t Term then u t v t Proof If t x where x V we get ult u x v x v t If t f ti tn where f is an n ary function symbol and t tn are terms we can conclude Lemma 3 1 2 f the valuations u and v coincide on all free variables of a formula p then u v iff v E v Proof If y p ti tn where p is an atomic formula and t tn are terms then every variable in each of terms occurs freely in the formula y So we can con clude u t v t fori 1 n using Lemma 3 1 1 which implies the assertion
28. and the automatic generation of candidates for loop invariants Currenly in this system only one data type is supported namely intergers More data types like character double float array etc can be added here to make it more robust One major concern of developing a programming language verifier is loop invariant In our system we prompted the user of this system to enter a loop invariant So at present it s the user s responsibility to provide the system with a valid loop invariant But this feature can be updated by searching for some appropriate candidates for loop invariants and provide the user to select a particular loop invariant 9 It will make the system more flexible and error free In this system we have implemented only the rules for the partial correctness as sertion The rule for the total correctness assertion can be implemented in future This feature will make this system complete if any complete model is used to interpret the syntactic materials Another possible work could be the addition of user defined functions in this system At present this system does not support any procedure definitions in the program So there is a chance of improvement here by implementing this feature which will make it a true programming language Only supported type of operation in the current system is INFIX So in future version support for PREFIX and POSTFIX operations could be added CHAPTER 7 CONCLUSION 67 Some other
29. ard applications of the induction hypothesis Now let us assume y Qy y with Q V 3 Now we will distinguish two different cases e If x y where x V and x does not occur free in y then y t x v By Lemma 3 1 2 we get u y iff u u t x v and hence the assertion e If x y we can conclude u E ylt x amp u H Qy e Tux u a y v t x for all some a Z ula y lula y t x y for all some a Z u a y u t x E y for all some a Z by Lemma 3 1 2 since t is free for x in Qy o u u t x a y E y for all some a Z since x Z y e u u t x E Qy e e u u t x E e Here the third equivalence is an application of the induction hypothesis Finally let us assume y a v Now free variables of y includes free occurrences 1 of variables in program a and any free variables of formula y whose occurrence CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 28 is not bound by any assignment statement of program a So that from induction hypothesis we can conclude u mz e t x gt u u t x malo 3 2 Soundness of the inference rules Soundness of a deductive system enforces that whatever can be derived in the deduc tive system is also valid That is rFo gt rTr Eo where I is a finite list of first order formulas py Yn and y is a first order formula The order and multiple occur
30. are based on first order dynamic logic But a high degree of automation and complexity of use make these existing systems very difficult to be employed as educational tools CHAPTER 1 INTRODUCTION 2 This thesis is about the implementation of a software verification tool for educational purposes It is targeted for the students learning software verification techniques Key features of this system are its ease of use and the visual exploration of every step of program verification The main requirement of this system is to define and implement a formal calculus for reasoning about programs Rules of Hoare logic have been implemented in this system to fulfill this requirement In addition to that we were also required to implement the rules of classical first order logic But those rules were already implemented for relational algebras by Bahar Aameri in her MSc Thesis 1 So we have reused her code with some modification to cope with the requirements of our system Chapter 2 Background on Dynamic Logic 2 1 Modal Logic Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality With the intention of distinguishing two sorts of truth necessary truth and mere contingent truth it was originally in vented by Lewis 1918 But the term modal logic is used more broadly to cover a whole class of different logics with similar rules and a variety of different symbol
31. asoning about programs we had to create some new classes in addition to the modification of existing classes The major changes in the code of that system are summerized below A new package named DL has been added which contains some classes to support different types of program statements For each type of these program statements a new button has been added to the GUI For Interacting to each of these buttons we had to make some changes in the classes of GUI package and some new classes has 50 CHAPTER 5 IMPLEMENTATION 51 been developed in the Rules package In the RelAPS system users are allowed to select a specific type of theory from a set of choices Depending on a specific choice a particular theory which includes a list of axioms theorems and a set of operators is loaded from the file directories But in our system we have only one type of theory which gave us the flexibility to hard code the operation information in the grammar file This modification in loading operation information leads us to make some major changes in the OpInfo class of Operations package A list of axioms that corresponds to the property of integer numbers is being loaded during the initialization of this system The combination of JFlex and BYacc J is used to generate the parser for formulas JFlex is a very popular tool for generating lexical analyzer in Java It has built in support for the parser generator BYacc J which is the Java extension to th
32. ationship between Hoare logic and dynamic logic where we presented how a dynamic logic formula can be used to represent the Hoare triple Then our exploration of first order dynamic logic started with the introduction the syntactic materials of the language of our system During the discussion of syntactic materials we get familiarized with programs formulas and test of first order dynamic logic This is followed by giving semantics to the syntactic constructs using the arith metic model we have used In the end of that section we discussed the satisfiability and the validity of formulas of dynamic logic Then we compared two versions of reasoning in first order dynamic logic uninterpreted reasoning and interpreted rea soning We discussed the interpreted version of reasoning that has been used in the system afterwards In Chapter 3 we have introduced the calculus of our system In the first section we presented the logical rules for first order reasoning and inference rules for dy namic reasoning that we have implemented in this deductive system This is followed by showing the soundness proof of these rules In the end of this chapter we have 64 CHAPTER 7 CONCLUSION 65 talked a little bit about the incompleteness of this system In Chapter 4 we have discussed the strength of this system to be used for edu cational purposes Here we have shown the explicit visual explanation of some proof steps in this system Then we ex
33. can derive the strongest postcondition of an assignment a t as sp pre a t Ja pre a a N a tla al It means there must be some previous value a of a such that if we use a for a then pre holds and the new value of a will be the previous value of t In other words sp pre a t pre a a N a tla al can be defined where a is a fresh function symbol For example we can consider sp a 2 a a 1 a 2 Na a 1 Managing sequential composition p1 p2 involves first the application of sp to p1 and then to p2 That means sp pre p1 p2 sp sp pre p1 p2 The advantage of using the weakest precondition transformation over the strongest CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 22 postcondition transformation is that it produces smaller verification conditions which encourages us to follow the weakest precondition approach For sp we need to intro duce an existentially quantified symbol a for denoting the pre assignment value of the changed variable whereas for wp an assignment amounts to a mere substitution in the postcondition Here the first order calculus is formulated in a sequent style We will have exactly one formula in the right hand side A logical calculus usually makes use of proof rules to infer a conclusion from a finite set of assumptions Given a sequence of formulas I and a derivation l F V application of a proof rule of the calculus to the derivation will result in a new derivation l gt F Wa
34. d ere et dtt e UE 2 2 1 Intuitive meaning of two modal operators of DL 2 2 2 Relationship of DL with Hoare logic 2 3 First order dynamic logic a od ne epa P Ue Ea SUE o A n ue xq ale hey Sens ae i a a aR e Soo Rah e o o cso hth e de duse ue Hd ee whet dur de where Wet 2 9 8 Satisfiability and Validity of Formulas 24 Reasoning in ROLL as a wt ar eee Melee nra poer Erg O O cuc 3 Calculus of the Deductive System 3 1 Inference Rules 3 2 Soundness of the inference rules 3 3 Incompleteness of this system 4 Overview of the System 4 1 Demonstration of the system x 4 3 x de amp Se ee Sy 4 2 Demonstration of the inference rules 5 Implementation 5 1 Brief explanation of source code 5 2 Class hierarchies 2n 6 User Manual 20 20 28 33 35 35 39 50 50 52 55 7 Conclusion 64 7 1 Summarization of work c ewe Boe SIDE SISSE EO 64 7 2 Comparison to other systems voee do RE ee Epa ee Ead 65 du URE A ek te te eh eee m US desig rl Ale beta ad endi 66 List of Tables 2 1 List of well known modal logic llle 3 Su Tndu ction Bale aaa E ven Ehe os AA dE A i ns 23 02 ACAD An end us Mee Ig la ve ut nete aq S IS d arde oe OS Red le mie 23 3 3 Logical rules for first order reasoning a a 25 3 4 Inference rules for dynamic reasoning 26 vi List of Figures 2 1 4 1 4 2 4 3 4 4
35. d here For example if we consider the first and the last occurrences of the arrow symbol in this example first occurrence represents the formula n gt 0 gt 1 0 0 and the last one represents the implication I r i i lt n gt r n m If we consider the whole program as a symbol C we can write 1 0 0 C Mr i A i lt n An additional proof of I r i A i lt n gt r n m and the implicit application of the consequence rule of Hoare logic gives n gt 0 C r n m As mentioned above the notation I r i is the placeholder for an invariant of the pro gram A loop invariant is used for proving properties of a loop This is a first order formula that should be true at the beginning of each loop iteration and is guaranteed to remain true on every iteration of the loop Therefore on the exit point of the loop both the loop invariant and the loop termination condition can be guaranteed It is not an easy task to find a sufficiently strong loop invariant for verifying a program property In addition to interactions on the level of first order reasoning human in teraction is required to handle loops in a program We will prompt the users of our system to enter a suitable loop invariant interactively for proving program properties in this deductive system 10 18 As we mentioned earlier we started the verification procedure from the bottom of the program Following the loop rule of Hoare logic we placed the f
36. demonstrated in Figure 6 4 Figure 6 3 The assumption of the current proof is displayed in the Assumptions window Figure 6 4 Activation of a left hand rule AndLeft CHAPTER 6 USER MANUAL 58 The application of this AndLeft rule is shown in Figure 6 5 where we can see mul tiple assumptions in the Assumptions window As a derivation can have multiple assumptions a list of assumptions can be placed in the Assumptions window From this list a user of this system is allowed to select a particular assumption in order to modify it _ raton Figure 6 5 The left hand rule AndLeft has been applied A user has the ability to select a term or formula in the Assumptions or Assertions window and drop it down to the Working Area window where an appropriate ax iom rule can be applied to the selected term or formula Figure 6 6 As we can see from Figure 6 6 an atomic formula is selected in the Assertions window which can be dropped down to the Working Area window by clicking on derivation button in Assertions window Result of clicking on that button is shown in Figure 6 7 Now we have one formula r n m in the Assertions window and three formulas i n i lt n andr i m in the Assumptions window If we select the variable n in Working Area window a list of arithmetic axioms will be loaded Among them if we select the axiom as shown in Figure 6 8 a new window will appear Purpose of this window is to let
37. e classical Berkeley Yacc parser generator 19 We had to make some major changes in the existing grammar file to cope with the requirements of formulas of our system In Bahar s system the only defined predicate symbols are and In the formula package some new classes has been added namely GreaterThanEq and LessThanEq to support the predicate symbols and In addition another class named DLFormula is also been created in the same package to support a dynamic logic formula that includes a program A class named FormulaVar has been added in the Terms package to take care of variables and constants in the formulas of our system In addition to that we had to make some minor changes in some other classes in Terms and Operations package for satisfying new requirements of finding or re placing variables The first step of our implementation was to define a proper language The language is comprised of a set of terms which includes variables constants or n ary function symbols where a function symbol could be any arithmetic operators like plus mi nus multiplication or division The next step involves the arrangement of a suitable interpretation of the entities of the languages The main work involved in this step is to search for a proper environment and a model and then defining terms value and formulas validity For this to work this system loads some arithmetic axioms during initialization and provide the user with the opti
38. e to interact with the system all the time With the help of user friendly GUI and step wise user interactions a learner of program verification techniques can easily get the idea of the methods of deriving a proof 4 1 Demonstration of the system This system accepts formulas of all possible forms discussed in Section 2 3 1 Figure 4 1 shows the result of entering a valid and invalid formula in this system Suppose the valid formula shown in the above example is entered into the system As we can see from Figure 4 2 the assertion window and the proof explorer window are updated accordingly with the entered formula text The button corresponds to implication rule is activated because this is an instance of implication formula Entering that button results the assumption window and assertion window to be updated with the appropriate text Figure 4 3 As the last statement of the program in the entered formula is an while statement the button corresponds to the application of loop rule gets activated Entering this button results the system to prompt the user to enter an invariant Figure 4 4 As we can see from the proof explorer window of Figure 4 5 three proof obligations are generated as the children of the while statement after taking the invariant from 35 CHAPTER 4 OVERVIEW OF THE SYSTEM 3 S Formula Editor i Formula Details n gt 0 gt r 0 i 0 while i lt n do r r m i i 1 od c
39. e procedure of program property verification using Hoare logic by hand For example as we start the verification from the bottom of the program and move backwards for the assignment rule we have the derivation IT p V a x as our assumption and our assertion goal is the derivation I E p x a V A popular approach to transform programs and specifications to first order verifica tion conditions is the weakest preconditions predicate transformer 2 Let us consider a program p and a formula post representing a postcondition formula The weakest preconditions transformer constructs a formula wp p post which is the weakest precondition of p with respect to post If wp p post holds before p then post holds afterwards Any other formulas having this property are stronger than the weakest precondition wp p post that means they logically imply wp p post Many of the popular program verifiers namely ES C Java2 Boogie JACK and Why use the weakest preconditions for generating the verification conditions 10 25 26 Let us consider an assignment statement a t For this assignment statement we can 20 CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 21 constuct the weakest precondition with respect to a postcondition post as wp a t post post t a where post t a denotes the the result of substituting all in stances of a by t in post For example wp a a 1 a 3 a 1 3 states that if the value of the variable a after t
40. each 1 e if the number is even it will be divided by 2 e if the number is odd it will be multiplied by 3 and then 1 will be added to the result of multiplication We can generalize the specific model Z which will result in a class of arithmetical models we can define a model Z as arithmetical if following are true e It has a copy of Z that is first order definable e It has first order definable functions that will code the finite sequences of el ements of the model Z into single elements and also has first order definable functions for corresponding decoding Importance of arithmetic models is significant because of the following facts e Most models emerging naturally in computer science are arithmetical For ex ample discrete models with recursively defined data types are arithmetical e Addition of appropriate encoding and decoding functionalities can extend any model to an arithmetical one Chapter 3 Calculus of the Deductive System In this chapter we introduce the calculus of the deductive system for first order dy namic logic In the next section we explore the proof rules we have implemented in this deductive system Then we will prove the soundness of these rules 3 1 Inference Rules In this system the main design criteria is the educational use of the system For this reason we designed the rules of this deductive system in a way so that the verifi cation procedure in this system is very close to th
41. efine programs independently from formulas In this paper we will use the term test to indicate the poor test version We have implemented the poor test version as part of if else and while program but we have skipped the notation in the implementation So the test in our implementation is not a standalone program it is used only as the condition of an if else or a while statement Regular Programs For the above mentioned set of atomic programs and tests the set of regular programs in this system is defined as e Any atomic program is a program i e an assignment statement is a program e If a and P are programs then o f is a program e If y is a quantifier free first order formula and a and f are programs then if y then a else 8 fi is also a program e If is a quantifier free first order formula and o is a program then while p do a od is also a program As we mentioned earlier the formula y occuring in the above programs must be a quantifier free first order formula Formulas In FODL a formula is defined similarly to a formula of first order logic with the addition of a rule for modality In our deductive system a formula is defined in the following way e The false formula is a formula e The true formula is a formula e Any atomic formula is a formula e If y is a formula then p is a formula CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 12 e If p and y are formulas then p A y is a formula e If p a
42. er the the main proof r n m in the Proof Explorer window As we have these two formulas and the formula in the Assertions window as assumptions the proof is done This is demonstrated in Figure 6 12 User of this system has the ability to maximize the Proof Explorer window to see a larger view of the generated proof tree To use this feature user will have to click on the Maximize button of the Proof Explorer Window Figure 6 13 CHAPTER 6 USER MANUAL 62 Dpr s P andi ce nandi oe ne re m Sd ptg te E Pots QucitmaMicsnamdi sacorsntm IT Clik ti r n m ji gt n Prerna Qnm Figure 6 11 Application of unification ol r Pm and ce nandi se neo re ntm 206r 2 amp Pots i li gt a dr medical n 25r ct gt A E P gt Y rarm je i m Figure 6 12 The completion of the main proof CHAPTER 6 USER MANUAL 63 Figure 6 13 Maximized view of Proof Explorer window Chapter 7 Conclusion In this chapter we will briefly review the contents covered in this thesis and compare it with some other theorem proving systems Then we will give some suggestions for extending the system in future 7 1 Summarization of work We started our discussion of basics of dynamic logic with the introduction of two modal operators of dynamic logic Then we introduced the rules of Hoare logic and gave an example of program property verification using Hoare logic Our discussion is followed by showing the rel
43. f the n20j y I 0 0 r 0 I r 0 I r 0 i 0 I r i I r i while i lt n do r i I r i 6 lt n y I r m i 1 r r m I r i 1 I r i 1 iH I r i od I r i a i lt n y r n m Figure Verification of program property using Hoare logic program r 0 we have I r 0 as the post condition Notice that I r 0 is a place holder for a formula an instance of the so called loop invariant Application of the assignment rule to this program statement towards backword direction will generate the pre condtion I 0 0 So we can conclude that this statement is correct with re CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 7 spect to the pre condition I 0 0 and the post condition I r 0 and its correctness is validated by the application of the assignment rule of Hoare logic In addition if we move from one statement to another the application of the sequencing rule of Hoare logic is implicitly there Suppose let us consider the first two assignment statements of the program in the given example We have used the pre condition of the second assignment statement 1 0 as the post condition of first assignment statement r 0 It is possible to use in this way because of the implicit application of sequencing rule of Hoare logic The downwards arrow symbols in the given example represents the logical operation of implication and the application of the consequence rule of Hoare logic is embedde
44. he assignment is to be 3 then the term a 1 must have to be equal to 3 before the assignment The weakest precondition of the sequen tial composition p1 p2 of programs p1 and p2 can be computed as wp p1 p2 post wp pi wp p2 post It means at first wp transformer is applied to p2 and post and then the outcome of this application is used as the postcondition which is to be established by p1 We can use the weakest precondition approach in dynamic logic in a natural way The dynamic logic formula p post is the weakest precondition of p with respect to post not in a first order form though This dynamic logic formula can be rewritten to a first order form by starting from the back and applying assignments to the post condition as substitutions in the above mentioned way For example if we consider a formula a t b t post we can first transform it into a t post t b and then into post t b t a An alternative to the weakest preconditions is the strongest postconditions predi cate transformers If we have a precondition formula pre and a program p this transformer constructs a formula sp pre p which is guaranteed to be hold after the execution of p if we start the execution in a state satisfying pre This strongest postcondition implies all other formulas with this property In the KIV tool the implementation of dynamic logic calculus for java programs is based on a variation of strongest postconditions 1 We
45. hlle i lt n dor rem i t od r a m fei mandi enandi n e ly eremi eiet r imandi en f nimandi ce n nd rot lt n e r entm et Figure 4 20 Application of the Assignment rule amp bd jt j Maize lE ET IO EE then i ied else is nst rs atm lif i n then n gt 0 and i 3 3 Cie m them ie else b 15 r n m i itl else i ntl fi r n m 9 Cm 21 i lt n gt i itl n gt 0 andi 3 maaa ener p n m and not i lt n gt i nel P icn s i id n mand not lt n gt i end r ate r n m Figure 4 21 Application of the if else rule CHAPTER 4 OVERVIEW OF THE SYSTEM 46 A ro tmo med ndr rm od tm Ir 455 Ade i ndo ro rome nondnm _ Oe doo tmo mel nr rm nod tme pr mo Rond i ndr rnm pa lod Ja m o Quart dro tmo mel nr rm iod tme y desto n mo rome ee tet pe m irte Adr mmm tamami omm and omm p mnm momo mmm mm don mandi andit od nm t i m and i cn Figure 4 22 Application of the loop rule CHAPTER 4 OVERVIEW OF THE SYSTEM 47 _ DI III Pes Figure 4 23 Application of the ForallLeft rule CHAPTER 4 OVERVIEW OF THE SYSTEM 48 Maximae Ciim forall a a lt b 3 dit pe Mame Proofs c P foraa a lt b Ga lt b Figure 4 24 Application of the ForallRight rule Sd Mame FE
46. ing a static method createProofs in ProofStyle class and then using ApplyRule method of IFRule class one proof obligation will be generated and passed to the GUI package The classes in the GUI package will then take care of updating the tree view of Proof Explorer section and Assertions and Assumptions window If the system detects any while statement as the last statement of a pro gram the user will be asked to enter a suitable invariant The system will then pass the invariant and the postcondition to the WhileRule class which will eventually generate three proof obligations from these inputs and return those proof obligations back to GUI class As we are asserting the formulas of this system about every integer number we were required to implement mathematical induction in our system For implementing this induction we have created a new button in GUI A new class named InductionRule has been added to the Rules package as well Clicking on the button corresponds to induction will take a input variable from the user and then three proof obligations will be generated after applying the induction rule on the working formula 5 2 Class hierarchies A formula of our system can take several forms Figure 5 1 Possible forms of for mulas include an atomic formula a binary formula or a formula with a program An atomic formula is a basic formula which could be generated using any predicate CHAPTER 5 IMPLEMENTATION 53 symbols and a bi
47. lex and the parser generator BYacc J for parsing formulas and programs has been used Acknowledgements First and foremost I offer my sincerest gratitude to my supervisor Professor Michael Winter for his guidance caring patience and providing me with an excellent atmo sphere for doing research Without his enthusiasms and support from the initial to the final stage of the development of this dissertation the completion of this thesis would never have been possible I must have to admit that one simply could not wish for a better supervisor I attribute the level of my Masters degree to his encour agement and effort I would like to express sincere appreciation to the committee members for their in valuable guidance and encouraging me with many insightful thoughts I would like to thank the department of Computer Science and the Graduate Studies of Brock University for the financial and academic support It was not possible to pursue my research in an anxiety free environment without the support I was pro vided with I would also like to thank my family members and friends for their constant as sistance and inspiration with the best wishes They were always there cheering me up and stood by me through the good times and bad T K D Contents 1 Introduction 2 Background on Dynamic Logic 2b Modal Doble d oso oe eed e qe ped Mute dioe en sod en E or aud d 2 25 Dynamic Logic cuoi mutus eee Be sour utl sre UU et
48. nary formula can be constructed using two atomic formulas In our implementation a term object is a part of a formula object A formula object is constructed using one or more number of terms Figure 5 2 Formula AtomicFormula BinaryFormula Not DLFormula Contradiction Quantifier t Ez A Equality LessThan GreaterThan LessThanEq GreaterThanEq And Or Implication Equivalence UniversalObj ExistentialObj Figure 5 1 Class diagram of Formula Formula ES Term Figure 5 2 Relationship between Formula and Term If any program statement is detected in the current formula depending on the type of last statement in that program an object of WhileStatement AssignStatement or IfStatement will be generated Each of these classes are a subclass of an abstract class Program Figure 5 3 This design of our program structure can allow us to utilize the advantages of Java polymorphism A term in our system can take three forms ObjectVal BinOp or FormulaVar For each of the quantification variables an object of ObjectVal will be generated An object of BinOp will be instantiated if the system detects any arithmetic operations in the formulas Finally for each of the variables and constants in the formulas a FormulaVar object will be created Figure 5 4 A Formula object and a Program object are defined by mutual induction A Formula CHAPTER 5 IM
49. nce in q x y is bound to the quantifier Vy As we do not have any quantification for the variable z it occurs free in p x y z Now we can consider a variable as a free variable of a formula y if it has a free occurrence in the formula y Substitution of free variables can be done by using the notation q ti 21 t4 x4 or e t z 1 lt i n which denotes the formula y with all free occurrences of x replaced with term t 1 lt i n If we consider two notations p x s y t and p x s y t these two notations are similar unless we have at least one occurrence of y in the variable s CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 13 If we have a program in the formula an assignment statement of that program can also bind free variables Let us consider an example which has a program within it n 0 x n 4 1 n x 1 y n 3 y 5 In this example of an implication formula the occurrence of n in the assumption part is free It also occurs freely in the first assignment statement of the program But the occurrence of n in the third assignment statement is not free any more be cause of the presence of second assignment statement which binds the free variable n So if substitution takes place for the free occurrences of n in this formula all occurrences of n will be substituted here except the occurrence of n in the third as signment statement of the program We can call a formula as a closed formula or sentence if it does
50. nd y are formulas then p V y is a formula e If p and y are formulas then w is a formula e If p and y are formulas then y w is a formula e If y is a formula and x V then Vz is a formula e If y is a formula and x V then dz y is a formula e If y is a formula and a is a program then a y is a formula Free and bounded occurrences of variables Let us consider Q as one of the two quantifier symbols V and d Now if a formula Qx y occurs as a subformula of another formula V we say that the scope of Qx within V is the formula y If an occurrence of a variable y in the formula V is not in the scope of any quantifier Qy with the same variable y such an occurrence of y can be called a free occurrence of y in V If we have Qy y as a subformula of a formula V and y occurs free in o then we can say that the occurrence of y in V is bound by the quantifier Qy Let us consider the following formula as an example dx Vy dx q x y p x y z In this example the scope of the first 4x is Vy dx q x y p x y z the scope of Vy is 4x q x y and the scope of the last occurrence of 4x is q x y The occurrence of x in q x y is bound to the latter occurrence of 3x The occurrence of x in p x y z is bound to the first occurrence of 4x but it occurs free in the subformula Vy 3x q x y and p x y z The occurrence of y in p x y z is free but it s occurre
51. not have any free occorrences of variables within it In a universal closure of a formula y the sentence is obtained by preceding y with enough universal quantifiers Vx to bind all the free variables of y 5 2 3 2 Semantics Assigning meaning to the syntactic constructs described in the previous section in volves interpreting programs and formulas over a first order model M Variable range is determined by the carrier of this model The values of variables are changed in programs by applying sequences of simple assignments and flow of control depends on the truth values of tests performed at different times during the computation Definition 2 Let us consider F as a set of function symbols and P as a set of predicate symbols Now a model M can have following data within it e The universe or carrier of the model M which is a non empty set e For each function symbol in the language f F which is of arity n there is a n ary function mu f M M e For each predicate symbol in the language p P which is of arity n there is a subset mu p M In a model a constant symbol is interpreted by one of it s elements Moreover a 0 ary predicate symbol can be mapped to subsets of M which is a set that has only one element within it There are exactly two subsets of this set the set itself CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 14 and the empty set modelling true and false respectively
52. of programs In this system we have used an interpreted version as this level of rea soning is very close to the actual process of reasoning about concrete fully specified programs The interpreted level of reasoning includes almost any task of verification of the correctness of an actual program We have considered a specific model of inte ger numbers with the usual arithmetic operations as the first order definable operation of subtraction and ged x y Let us consider as the first order definable operation of giving the greatest common divisor of x and y Then we can consider the following formula as Z valid DL formula x z A y y1 x y gt 1 gt a x gcd x1 y1 where a is the following regular program while x y do if x gt y then X X y else y y x od This formula states the partial correctness of an actual program for computing the greatest common divisor which is interpreted over model Z Let us consider another example of formula over Z Vx x21 gt while x gt 1 do if even x then x x 2 else x 3 x 1 CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 19 fi od where integer division is represented by and the relation even checks whether it s argument is even or odd This formula corresponds to a famous problem in num ber theory namely the 3x 1 problem 5 24 In this formula if we start with an arbirary positive integer then after executing the following two operations repeatedly we will eventually r
53. on to select a particular axiom to apply from a list of appropriate axioms in the derivation window User of this system can select a formula or term in the assertion or the assumption window and can drop it down to derivation window After applying appropriate derivation rules user can send the corresponding derived formula or term back to the assertion or CHAPTER 5 IMPLEMENTATION 52 assumption window There was already a class developed in RelAPS system named Unifier to establish an environment for mapping from one term to another But we had to make some changes in different classes of GUI Formulas and Operations package to adjust the unification operations with our requirements The classes in the ProofFactory package are used to control the application of the rules and the GUI package is used to make necessary changes in the interface of the application To control all instances of the rules of program reasoning namely WhileRule IfRule and AssignmentRule a class named DLProof is created in Proof Factory package T his package also contains one class for each of the derivation rules In GUI for every derivation rule we have a button which get activated depending on the context of a working formula Now for example we have a program in the formula and the last statement of that program is an if statement In this context the button corresponds to the if rule will get activated Entering that button will first create a new proof us
54. or precondition y and an output condition or postcondition w These two conditions are properties of input state and output state respectively The program is supposed to terminate in a state where the output condition is true given the input state satisfies the input condition Now the program is called partially correct with respect to the input output specification q w if the following condition is true e Whenever the program is started in a state where the input condition q is true then if the program ever terminates it does so in a state where the output condition w is true So the definition of partial correctness does not ensure the termination of the pro gram In contrast we can call a program totally correct with respect to an in put output specification y v if the following two conditions are satisfied 14 15 16 17 e The program is partially correct with respect to the specification e The program terminates whenever it starts in a state satisfying y CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 5 2 2 2 Relationship of DL with Hoare logic Hoare logic is a calculus that can be used to prove partial correctness assertions so called Hoare triples which take the form 3 p efv where p 4 are formulas and c is a command or program It states that if the pre condition y is true before the execution of the program c and the program terminates then the post condition v is satisfied after the program execution For
55. ormula I r i A i lt n after the exit point of while loop and the formula I r i before the entry point of while loop Now as the assumption of the loop rule that is the formula we have above the bar suggests we placed I r i before the exit point of while loop and I r i i lt n after the entry point of while loop Now we work backwords by applying the CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 8 assignment rule of Hoare calculus As we move backwards the sequencing rule and the consequence rule of Hoare logic are implicitly there and incorporation of these rules let us to move from down to top of the program The verification of properties of the above program requires proof of the following three steps e n gt 0 gt I 0 0 e I r i lt n gt I r m i 1 e I r i i lt n gt r n m 1 2 Figure 2 1 Comparison of values of i and r in the given example Now for verifying program property using Hoare logic we need to determine the invariant of the program An invariant of a program is a first order formula which is valid at the beginning of each loop iteration 10 By comparing the values of i and r we can determine the invariant of the above program which can be given as I r i r i m i n Using this invariant proofs of the three steps are illustrated below Proof of 1st step e By applying the arithmetic axiom n gt 0 0 lt n we can get n gt 0 e 0 0 0 A 0 n I 0 0
56. ormula y is comprised of the set of all valuations for which the formula is true If the formula is true for a valuation u we can write u mz q where u S Let us consider the following formula y as an example x 0 gt y 4 while x gt 3 do x x 1 yy od y 5 Let us consider a valuation u that satisfies the left hand side of the implication i e u x 0 After executing the program we obtain the valuation u 3 x 24 y since u u 3 x 24 y is an input output pair of the program So after the execution of this program the content of y is 24 As this does not satisfy the given formula we can write u mz p Semantic definitions for the constructs of program and formula can be given as follows e mz a mz a o mz B u v 3w u w mz a and w v mz 8 e mz while y do a od u vy Jn gt 0 Juo Un U Uo v Un for uj mzlp and ui ujj1 mz a for 0 i lt n and un mz y CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 17 m m m m m z if y then a else 8 fi i u v where u mz q and u v mz a u w where u mz p and u w mz 6 z false z true S zla gt b F u Va b u a gt u b g a lt b u Va b u a u b e mz a gt b 4 fu Va b u a gt u b e m zla lt b fu Va b u a lt u b y e mz a b f u Va b u a u b e m em em m m
57. plored the strategy we followed to implement this deductive system We broke down our discussion of implementation in two parts In the first part we briefly explained our source code Here we have learned about different packages of our system and how the system is responding to the user interations This is followed by the discussion of class hierarchies where we presented the class diagrams of some important classes of our system We also presented the relationship between some classes of our system Finally we have presented a user manual for this system Our intention was to make the system extremely user friendly For this reason in that chapter we showed how a proof can be carried out in this system with a detailed explanation We presented every step of proving an example proof with the help of screenshots 7 2 Comparison to other systems The main purpose of developing this system is to meet the necessity of an educational tool for the beginners of program verification techniques Examples of some of the existing systems which are very popular in this field of program verification is KIV tool and KeY system These systems were mainly developed for commercial purposes Different industries can use these system to fulfill the requirement of real program verification For this reason these systems are very much efficient in terms of the time and the space complexity and the most of steps of program verification are automated there So
58. r the loop invariant i 0 r i m and i lt n Figure 4 5 While rule has been applied For the purpose of equational reasoning users are allowed to select a formula or term from the assertion or assumption window and drag it down to the derivation window In derivation window depending on the selection of user a list of axioms is loaded User can apply an appropriate axiom from the list to get the desired derivation An example of the application of axiom rules is shown in Figure 4 6 Once the derivation has been finished in derivation window user can replace the selected term or formula in assertion or assumption window with the derived term or formula As we can see from the Figure 4 7 the identity relation in the assertion window is trivial which proves the validity of this portion of this proof If the modified formula in the assertion window is the same as one of the current assumptions or if it is trivial the system will recognize this part of the proof as a valid proof This is reflected in the proof explorer window with a tick mark shown to the left of the proved portion Figure 4 8 This feature of highlighting a sub proof will confirm the user of this system that they are in the right track of deriving a proof CHAPTER 4 OVERVIEW OF THE SYSTEM 38 File View Tools Help D u cH EZ Maximize S n gt 0 gt r 0i Ojwhile i n do r r myi i 1 0d r n m S r ji
59. remas r n m 4 Messages Formula is syntactically correct 36 j Formula Editor j Formula Details n gt 0 gt e 5 Open Formula Text r 0 wh NT TRN Save Formula Text while i lt n do d r r m i i 1 od 2a Messages Syntax Error Syntax error at while E RelAPS D ult Wo File View Tools Leo Proof Explorer n gt 0 gt r 0 i O while i lt n dor r m i i 1jod r n m A ld H E7 Maximize H Proofs 3 n gt 0 gt r 0j O while i lt n do r remi i 1 od r n m Ly RelAPS Default Workspace File View Tools Help D gc d sd Er 0 uy amp YB n gt 0 gt r 0i Ojwhile i n do r rtm 10d r n m 3 r 0 1 O while i lt n dor remi i 1 0d r n m while i n do Y rm 4 it1 od r n m Figure 4 3 After application of the implication rule user updated data The assumption and the assertion window are also been changed with the CHAPTER 4 OVERVIEW OF THE SYSTEM 37 ZEAN Ir 0 n gt 0 i 0 while i lt n do S n gt 0 gt r 0i Owhile i lt n do r remi i 1 0d r n m KA r 0 1 O while i lt n do r r m j i 1 od r n m py Please Enter the Invariant jrei mandi n Figure 4 4 User is asked to ente
60. rences of a formula within I are treated implicitly By the notation y we donote the list I extended by a first order formula g This is the least requirement of any logical system The following lemma will il lustrate the soundness of our first order calculus Theorem 3 2 1 Let T be a sequence of first order formulas 1 Pn and V be a first order formula If V E V is valid then T V holds Proof The proof is done by induction on the derivation I V Base cases We have several base cases All the axioms we have for the integer numbers are true because of the choice of the model i e the set of integers The axioms of the table above are trivial VI Here V Vx V and the derivation we have is qi Yn F V The vari able condition implies that there is no free occurrence of x in any of q Yn Let us consider Z be the model of integer numbers and u be a valuation with u fori 1 n Using the Lemma 3 1 2 we can have u a x E vj for all a Z and i 1 nj Now using the induction hypothesis we can conclude u a x V for alla Z and therefore u V VE In this case V V t x and we have a derivation qi o F Vx V Now let us assume u be a valuation with u v fori 1 nj So by induction hypothesis we can conclude u Vx Y and in particular u u t x H V So we can get u H V t x
61. rivation tree will have the premises of the rule as its unfinished leaf sequents CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 6 For the purpose of dynamic reasoning we have implemented the rules of Hoare logic in a more compact form But these implemented rules are equivalent to the corre sponding rules in Hoare logic We had to implement three rules of Hoare logic namely assignment rule conditional rule and loop rule The skip rule is trivial and the rest of the rules namely sequencing rule and consequence rule are implicitly there We will introduce the implemented version of these rules in detail in the following chapters Let us give an example of program property verification using Hoare logic In this ex ample we have formulas n gt 0 and r n m as the pre condition and the post condition of the program respectively The verification method is started here from the post condition and the rules of Hoare logic are applied backwards Instead of using the tree form of a derivation here we annotated each of the program statements with a pre condtion and a post condition In this example as the last statement of the program is a while statement the loop rule of Hoare logic is applied first Here each program statement is correct with respect to the corresponding pre condition and post condition and the correctness of each statement is validated by the application of a specific Hoare logic rule For example if we consider the first statement o
62. rogram within it the last statement of which will determine the activation of a specific button For example if we have a program in the current proof and the last statement of the program an instance of a while statment then the corresponding button for the application of while rule will be enabled The system has two seperate windows namely Assertions and Assumptions win dow to let the user know about the goals and assumptions of the current proof The Assertions window is used for displaying the assertion of the current proof which is the right hand side of F in a derivation The text area of the Assertions window is used only to display the current state of the assertion being worked with The user are allowed to work with only one assertion at a time This is specified by clicking on the appropriate assertion in the tree view of the Proof Explorer window Figure 6 2 95 CHAPTER 6 USER MANUAL 56 Figure 6 1 T he user interface of this system Figure 6 2 T he current goal is displayed in the Assertions window The Assumptions window is used to display the assumptions that are associated with the current proof This corresponds to the left hand side of in a derivation i e T Figure 6 3 shows the assumptions of the current proof in the Assumptions window A left hand rule for first order reasoning can be enabled based on the selection of an CHAPTER 6 USER MANUAL 57 assumtion in the Assumptions window This is
63. s A list of well known examples of modal logic is given in Table 2 1 11 12 Logic Symbol Expressions Symbolized Modal Logic It is necessary that It is possible that It is obligatory that It is permitted that It is forbidden that It will always be the case that It will be the case that It has always been the case that It was the case that X believes that Deontic Logic Temporal Logic 931353070 UJ gt Doxastic Logic Table 2 1 List of well known modal logic CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 4 2 2 Dynamic Logic Dynamic logic DL is a modal logic which is originally intended for reasoning about computer programs In this logic we have countably many O and operators In fact for each program there exists a O and a operator 13 2 2 1 Intuitive meaning of two modal operators of DL If is a formula of DL and a is a program then the meaning of the two modal operators can be intuitively described as e o every computation of a that terminates leads to a state satisfying q e 0 there is a computation of a that terminates in a state satisfying q In the above definitions a asserts the total correctness of a program In general a program is designed for implementing some functionalities which can be expressed formally in the form of an input output specification Such a specification involves an input condition
64. such u exists So I ay V is always true R It is trivial AR In this case V i o and we have derivations I F o and T F s Now assum ing u be a valuation u E P holds From the induction hypothesis we can conclude u y and u E v which implies u 4 a and hence u E V VR In this case Y y V p2 and we have a derivation Hy Now assuming u be a valuation u holds By the induction hypothesis we can conclude u v1 and by the definition of we can get u E qw V v gt R In this case V y 2 and we have a derivation DL p F qs Now as suming u be a valuation u P holds If u y holds then from the induction hypothesis we can get u ws By the definition of we can conclude u y gt p2 If u Ay then by the definition of E we can get u v1 gt Q2 gt R In this case V q a and we have two derivations T F 4 qs and D F 2 gt y Now assuming u be a valuation u PF holds Then from the induc tion hypothesis we can get u 1 gt 2 and u y2 gt y So by the definition of we can conclude u g1 v aR In this case Y p and we have a derivation T o F L Now assuming Z be a model of integer numbers and u be a valuation u F holds As Z satisfies y we can conclude u L from the induction hypothesis But this is a contradiction So
65. system Semantic completeness of a formal deductive system is the converse of soundness of that system If all of the tautologies of a formal system are theorems then we can call that formal system semantically complete That is for a formal system is to be semantically complete the following property should be satisfied Es Y gt Fs y In 5 Harel presented some simple axiom systems for various programming lan guages which are arithmetically complete This means that DL formulas can be effectively converted to a set of predicate logic PL formulas using these systems The generated PL formulas can be considered as verification conditions and have to be proved using first order reasoning These systems use Hilbert style axiomatization which involves a huge number of axioms and very few inference rules This feature makes these systems almost impossible to be implemented for practical applications 6 For the following two reasons our system cannot be complete e Implementation of the Hoare logic rules for dynamic reasoning e Choice of the model The set of integer numbers As the main focus of this system is to be used as an educational tool we have imple mented only the rules of Hoare logic for the partial correctness assertion It was not necessary for us to implement the rule for the total correctness assertion because the implementation of the Hoare calculus was sufficient for ensuring the educational use of this system
66. system for reasoning about programs It can be described as a mixture of three complementary classical ingredients first order predicate logic modal logic and the algebra of regular events These make it rich in both theoretical and practical aspects 5 Dynamic Logic and other program logics are intended to facilitate the process of producing programs correctly For the application of formal verification tools we need to have a formal specification of correctness for the verification tools to work with In general we can control the behavior of a program by a formal description of correctness specification That means if the behavior of a given program satisfies a correctness specification then this program is correct with respect to that specifi cation The effectiveness of dynamic logic for program verification motivated several exist ing program verification tools implementing various variations of calculi based on dynamic logic Example systems include KIV Karlsruhe Interactive Verifier and KeY system 4 21 KIV is a formal system development tool which supports proofs for specification validation design verification and program verification using an ad vanced interactive deduction component based on proof tactics It is a very powerful tool for program verification which can be used for professional purposes On the other hand the KeY System is a formal software development tool for the verifica tion of object oriented softw
67. tem very well suited for educational purposes As an interactive program verification tool user interactions are required for the application a proof rule to proceed to the next step of verifica tion The key feature of this system is the visual explanation of the application of these rules which makes it a convenient one to the learner of the program property verification techniques CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 23 Inference rules are applied for carrying out the logical operations There are three different types of rules we have in our calculus e Model specific rules and axioms e Rules for first order reasoning e Rules for dynamic reasoning Model specific rules and axioms include the induction rule and the axiomatic rules for the set of integer numbers Z Mathematical induction is a method of mathematical proof which is implemented to establish that a given statement is true for all integer numbers Tres Ps ele t a Teh ole M Induction Table 3 1 Induction Rule As we mentioned earlier a derivation is actually a tree with the premises as leaves applications of rules as nodes and the conclusion as the root This tree will be ended at axiom rules which do not have any premises The axiomatic rules that have been listed here are the axioms we currently have in this system This list can be extended with the newer axioms if equational reasoning of a term or formula requires the application of those axioms
68. these systems are not concerned about making everything easy and nice for the learners of the program verification techniques On the other hand in this system we have chosen the calculli of the rules of the Hoare style proofs which is very similar to how beginners learn As we have used the weakest precondition transformation over the strongest postcondition transformation we did not have to introduce any existentially quantified symbol for denoting the pre assignment value of the changed variable which is the case in KIV tool Because of this feature an assignment operation can be done merely by a substitution in the postcondition in CHAPTER 7 CONCLUSION 66 this system Some other features which make this system suitable to be used as an educational tool are the choice of the first order calculus and the support of equational reasoning As the first order calculus we have chosen is based on natural deduction it is very similar to doing it by hands In addition to this a user of this system has the flexibility to do equational reasoning exactly in the way we do it in a piece of paper So all these features make this system a suitable one over the existing program verification tools in terms of educational purposes 7 3 Future work There is a plenty of further work can be done to improve the capabilities of current system and to enhance it s robustness The main focus in the future work should be on the inclusion of new data types
69. variables of y includes free occurrences of variables in program a and any free variables of formula q whose occurrence is not bound by any assignment statement of program a So that from induction hypothesis we can conclude UF YSVEFY Lemma 3 1 3 If we consider u as a valuation t t Term as terms and y as a formula then u t t x u u t z t Proof This assertion is shown by induction below If t y where y V we distinguish two cases e f x y we can get u t t x uy u u t z x u u t z e If x Z y the valuations u and u u t z coincide on all variables in t Now using Lemma 3 1 1 we can conclude u t t x uy u u t x y ulu t 2 t CHAPTER 3 CALCULUS OF THE DEDUCTIVE SYSTEM 27 tn we can get immediately u t t x mz u ti t x u t t x by substitution mz u u t z t1 u u t x t by induction hypothesis 0 21 Lemma 3 1 4 If u is a valuation t is a term and y is a formula then u mz e t z iff ufa t lt mz p Proof If y p ti tn we can conclude u E plt x u FE plti t x t t x by substitution e altilt x Wealt x mz p e Ot uh a tn mato e v u t x E p t te e ula t x E v If the case y is one of the following formulas true false y Y1 A Pa Y1 V Ya Q1 Y then it is straight forw
70. y mutual recursion Let us consider a finite set of vocabulary gt f g p r where f g and p r denote typical function symbols and predicate symbols of the vocabulary gt Each of these function and predicate symbols is implicitly associated with a fixed CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 10 arity the number of arguments it has Functions and predicates of arity 0 1 2 3 and n are called nullary unary binary ternary and n ary respectively We will use a countable set of individual variables V zo 11 Nullary function symbols are called constants and nullary predicate symbols are called propositions of the language Definition 1 The set Term of terms is defined recursively by the following e Each variable x V is a term i e V C Term e lf f Fis an n ary function symbol and ti to t Term are terms then f t1 t2 14 Term Examples of terms include f x y z or f g x x g x y y where f is a ternary function symbol and g is a binary function symbol In this system we have defined arithmetic operators PLUS MINUS MULTIPLICATION DIVISION and EXPONENTY as the function symbols In addition here we have implemented the INFIX notation of writing arithmetic expressions which dictates us to write expressions in the form of x y instead of x y or x y So a term in this system can take the form of a b a b a b a b or a b where a Term b
71. y 2 x ulule u y 2 y y ulule uly fa u x u y uy 9 Now if u satisfies the left side of the formula i e if u x 0 and u y 2 then after executing the program we can get ulu a u y 2 ulo uy u y y w u x u y 0 2 2 and ulu x u y x llule u y u y yly ula uly u y 0 2 2 4 So this state satisfies z y x if u z 2 Assignment Statements Every program is associated with a binary relation which is called the input output relation mzla C S x S and every formula y is associated with a set mz p S7 These two sets are defined by mutual induction on the structure of y and a The semantics of the assignment statement given below will be used as the basis of the inductive definition of programs and formulas e Meaning of the assignment statement x t is given by the following binary CHAPTER 2 BACKGROUND ON DYNAMIC LOGIC 16 relation mz x t u u u t x u e S Programs and Formulas Interpretation of compound programs and formulas are given by mutual induction on the structure of program a and formula y As we mentioned earlier if we consider u and v as the beginning valuation and the ending valuation of the program a respec tively we can write the pair u v as u v mz a where u S v S7 The semantics of a program is the set of all possible input output pairs On the other hand the semantics of the f

Download Pdf Manuals

Related Search

Brock_Das_Tuhin_2012

Contents

Download Pdf Manuals

Related Search

Related Contents