Home

The Z/EVES 2.0 User's Guide - University of Waikato: Department of

1. 7 8 By the definition of _ _ it is enough to show R P dom R x ran R By theorem inPower this is equivalent to Ve Re e dom R x ran R So let e R be arbitrary we need to show e dom R x ran R Since e R and RE X gt Y we have ec Xx Y Therefore there exists x X and y Y with e x y by theorem inCross2 e E Rand e z y So x dom R Similarly y ran R Thus x y dom R x ran R and since e x y the proof is complete Three steps in this chain 4 6 and 7 need filling in and we will make a lemma for each of them theorem thm1 X Y VR X SoY eERT gt CEEX x Y theorem thm2 X Y VR XuoYe 1 y R gt xEdomR Z EVES Project TR 99 5493 06a 53 theorem thm3 X Y VR X Ye rt y eR gt yeranR With these three lemmas in place we can turn to the main theorem theorem relationInDomCrossRan X Y VR Xo Y eRe domR gt ran R The first step in our argument used the definition of gt There are two occurrences in the goal so we direct Z EVES to expand the one we want by the command invoke dom X Y R rel ran X Y R which gives the goal ReX e Y gt R c P dom X Y R x ran X Y R The second step was to use theorem inPower As this is a disabled rewrite rule it can be applied by selecting the predicate right clicking and selection inPower from the Apply to predicate submenu of the pop up menu This res
2. NN we will conclude dom N N g N This is not useful when we write dom g we mean dom Z Z g So a generally useful theorem needs to state AEPXABEPYAFEA gt B gt dom X Y f A Several theorems in the Toolkit have a similar form with seemingly irrelevant extra variables The theorem f A B A x dom A f x B has a similar problem with the generic actuals for dom This problem is compounded by the difficulty in making this fact be applied automatically In consequence there are a number of special cases of this theorem in the Toolkit One of these states s E seqX A xz doms gt s i X asserting that any element of a sequence lies in the declared element type of that sequence This really means dom Z X s which is inappropriate if X is not a type 4 1 2 The current theory A proof is conducted in a particular theory that is in the context of a particular collection of definitions axioms and lemmas This context is fixed for any given proof in Z EVES but is different for different proofs A theorem appearing as part of a specification has as its context all the definitions and theorems preceding it thus avoiding circular proofs where theorem A uses theorem B in its proof and vice versa This treatment of the context is simple and easily managed but has a sometimes inconvenient consequence If in the course of a proof a user discovers the need to introduce a lemma this lemma needs to be introduced into the cont
3. A schema can have a predicate that is not satisfiable If such a schema is meant to describe the state of a system then that system is impossible if it is meant to describe an operation then the operation can never be successfully invoked In either case the specification is probably in error Such an error is local however in that theorems proved in a specification having only local inconsistencies are in fact theorems and specifications of other components of a system may still be meaningful It is easy to express the satisfiability of a schema S using the predicate 4S e true Sometimes a more impressive alternative is available many specifications give an initialization schema of the form Init_S S P where the predicate P further constrains the state In such a case showing 35 e Init_S not only shows that S is satisfiable it also shows that initial states are possible For example given the corrected schema declaration Personnel above and the initialization schema InitialPersonnel Personnel salary we can show theorem InitialPersonnellsPossible J Personnel e InitialPersonnel as follows proof invoke prove instantiate boss_of invoke prove 3 2 Exploring a Specification Formal specifications offer opportunities that are completely absent from informal prose descriptions Formal specifications can be manipulated according to rigorous rules of logic allowing properties
4. e New Paragraph can be selected from the Edit menu This exposes the Edit window described in Section 2 2 5 which allows the paragraph to be composed The new paragraph is added to the end of the specification e Paragraphs can be imported from a TX file as described in Section 2 5 e A Paste operation inserts the contents of the clipboard immediately before the paragraph containing the insertion point where the blinking cursor is in the specification window Paragraphs in the specification window can be checked modified deleted or moved A paragraph can be checked by double clicking on it or by selecting it right clicking and selecting Check from the pop up menu Selecting Check up to here checks all preceding paragraphs before checking the selected paragraph The entire specification can be checked by selecting Check all paragraphs from the Command menu While paragraphs are being checked most Z EVES functions are disabled However it is still possible to select different windows and to scroll them The Abort button can be used to stop checking A paragraph can be modified by selecting it right clicking and selecting Edit from the pop up menu This brings up the Edit window with the selected paragraph as its initial contents When the edit is finished the revised paragraph replaces the original The revised paragraph is not checked Following paragraphs will also become not ch
5. from the File menu brings back the Specification window with a revised definition of LogSys The status bars both hold question marks since the revised version of LogSys has not yet been checked After double clicking on the revised paragraph the check succeeds and both status bars show Y Continuing in this way we can add and check the remaining three paragraphs shown at the start of this section When schema Login is checked the syntax status bar holds a Y as there are no syntax or type errors but the Proof bar holds a N Ep pa 2200 Eager MN Syntax Proof This paragraph has an associated goal that has not been proved This is a domain check asso ciated with the paragraph as explained in Section 3 1 2 We will ignore it for now The work done so far can be saved by selecting Save or Save As from the File menu Work on the specification can be continued later by opening the saved file 14 Z EVES Project TR 99 5493 06a 2 4 Analysing a Specification As will be explained in more detail in Chapter 3 Z EVES supports various kinds of analysis that go beyond type checking We will illustrate the mechanics of doing the checks here and explain their significance in Chapter 3 One simple check is to see whether the initial state is satisfiable This will show both that the state schema is consistent and that there are possible initial states We can add the following conjectur
6. Woman groom Man e pre Wedding After checking this paragraph we can work on its proof The command prove by reduce results in the predicate wife_of Man gt Woman A bride Woman A groom Man gt wife_of U groom bride Man Woman The various schema definitions have been expanded the one point rule was applied and some simplification was done The predicate asserts that the updated value of wife_of must be a partial injection We can explore this predicate further The Z EVES library has many rewriting rules that are not applied automatically If a part of the goal predicate is selected and the right mouse Z EVES Project TR 99 5493 06a 27 button is pressed any of these disabled rewrite rules that apply to the selected part of the formula can be seen in the Apply to predicate or Apply to expression submenu In this case selecting wife_of U groom bride Man Woman e g by sweeping the mouse across it or by clicking inside it enough times there is only one applicable rewrite rule cupInPinj This theorem describes when a union is a partial injection and is disabled so that it is not normally applied automatically by a Z EVES step The Toolkit author made this choice because it seemed unwise to introduce the rather complex replacement predicate of this rule without the user s consent Selecting this name from the Apply to predicate submenu results in a lengthy predicate we w
7. Deposit amount 100 amount With the test cases defined we can simply use schema expansion to see what happens For example trying Test3 is possible by defining a theorem theorem TryTest3 Test3 In the proof of this theorem the command prove by reduce results in the formula balance 520 Some caution is advised in the use of test cases sequential composition of operation schemas does not exactly correspond to the sequential composition of the operations In particular it does not account for cases where one operation results in a state not in the precondition of the next Furthermore in a schema composition any two outputs of different operations if they have the same name must have the same value 3 2 6 Test theorems A useful way of assessing a specification is to prove theorems about it Such theorems are formal spot checks of a specification For example consider the ticket generating system defined in Section 3 2 4 which we repeat here Ticket given PZ Init Ticket given Z EVES Project TR 99 5493 06a 33 New A Ticket t Z t E given given given U tl We can show that two successive invocations of the New operation will not return the same ticket value TwoTickets New g New t2 t theorem twoTicketsNotSame V TwoTickets e t2 4 t which is easily proved by the prove by reduce command 34 Z EVES Project TR 99 5493 06a Chap
8. First a function can be applied outside its domain as in 1 div 0 maz Z or N Second a definite description term is not meaningful if there is not a single value satisfying the predicate Examples are wx Z x x for which there is no possible value of x satisfying the predicate and px Z x gt 0 for which there are many possible values Different Z authors have adopted different positions on undefinedness in Z e Spivey 13 states that any atomic predicate containing an undefined term is indeterminate meaning that it has a truth value so classical logic applies but he deliberately does not tell us whether it is true or false e The draft ISO standard for Z 5 specifies that an atomic predicate containing an undefined term is false However the draft is not definitive on which terms are undefined the semantics leaves open the possibility that say yx Z x gt 0 may or may not have a value Furthermore undefinedness is not inherited in all expression contexts e g if 1 div O is undefined the set x 1 1 1 div x is defined and has the value 1 1 as any undefined value is simply ignored in a set comprehension e Some authors e g Woodcock and Davies 15 use strong equality which is true if both arguments are undefined or if both arguments are defined and equal There is also some question about which expressions can be defined even when some subexpres sion is undefined e g the set comprehension ab
9. _seq _iseg prefix disjoint partition bag inbag pre Logical Symbols i A v Basic Symbols P x e a ne 7 Boxed paragraphs can be entered by first selecting the appropriate box type from the Edit menu which clears the editor and inserts a schema axiomatic or generic box The name decla rations and predicates can then be inserted into the appropriate parts of the box Alternatively boxes can be drawn by selecting the individual box characters from the palette Keyboard shortcuts are also available for most special characters For all letters except j and v control letter is bound to the corresponding Greek letter control shift letter to the capitalized Greek letter The most commonly used Greek letters are in the following table Symbol A H 0 A Key Ctl 1 Ctlm Ctlq Ctl D Ctl X Other symbols are available as shown in the following table Symbol a A V gt gt Vv Key Alt Alt amp Alt v Alt Alt Alt A Alt E Alt Symbol P x 0 E U N Key Alt P Alt x Alt e Alt 0 Alt z Alt c Alt U Alt I Symbol gt gt o lt gt lt gt Key Alt j Alt f Alt o Alt r Alt t Alt y Alt u Symbol N Z lt gt F D 1 Key Alt N Alt Z Alt lt Alt gt Alt F Alt Alt Several Z characters are similar in appearance and should
10. by a prove command This results in the goal a AEPX AA EPX ABEPX A B EPX MA EPA AB EPB Are A MA xEB A7 32_0 AN X B e true gt x B We still want to argue by contradiction we can use a split command to suppose x B then simplify Splitting is easy by selecting the desired predicate here x B right clicking and selecting Split on this predicate from the pop up menu Following this with a prove command finishes the proof 5 2 Planned Proofs In a planned proof some time is spent in developing an informal proof of a theorem before a Z EVES proof is started The informal proof is used as a guide to the development of the formal proof In the simplest case an informal proof has the form of a sequence of lines each of which is a predicate that is either an instance of a previous theorem or which follows from earlier predicates in the sequence and where the final predicate is the theorem to be proved For example given Q X Y R Y gt Z and S P Y we can prove Q S 3 R Q3 S lt R using the following steps 1 Q gt S Q3idS by Toolkit theorem compIdRight 2 Thus Q gt S 3 R Q id S 3 R by Leibniz Law the substitution of equals for equals 3 Q3idS 3 R Q3 idS 3 R by Toolkit theorem compAssociates 4 id S3 R S lt R by Toolkit theorem compldLeft 5 Thus Qs id S3 R Q3 S lt R by Leibniz Law 6 Q S 3 R Q3 S lt R by
11. exposes a proof window with this predicate NewAccount as the goal Issuing the command prove by reduce then results in the new goal predicate account ID Account A accounts dom account A users P Client A id ID A account account O id 0Account balance 0 users users A accounts id U dom account A 7 users A id dom account where all the schema references have been expanded and some simplification has occurred In particular the one point rule applied to eliminate the existential quantifier and some redundant conjuncts were eliminated After the exploration is complete the theorem paragraph should be deleted 3 2 2 Preconditions The Z style of specifying operations is relational an operation is specified in the normal convention as a relation between initial and final states This style has a number of advantages but has the disadvantage of leaving the precondition of an operation implicit For example an operation 26 Z EVES Project TR 99 5493 06a Op n n N n n 1 describes only situations where the initial value of n is non zero The conventional interpretation of this is that if Op is invoked with n 0 there are no guarantees about what might happen the operation might fail catastrophically might never terminate or might yield some ordinary result state which need not even satisfy n N more generally such an operation may result in
12. 2 3 and 5 Such a proof can be presented to Z EVES as a series of use commands one for each line of the proof possibly after some theorems are stated A theorem is introduced for each step that deduces a predicate from some prior predicates this theorem asserts that the earlier predicates imply the conclusion Where a step brings in a prior theorem the use command does so as well Where a step deduces a new predicate from prior predicates the use command brings in the associated theorem Finally a simplify or prove command completes the proof Of course the theorems that 50 Z EVES Project TR 99 5493 06a are introduced are themselves in need of proof However each of these lemmas is usually simpler than the original theorem In practice it is not always necessary to have a theorem for every line of the proof some steps are so simple that the final prove command can make them automatically This is an advantage that the prove command has over the simplify command in completing a proof it is more powerful in filling in gaps in the proof For the example above we need no theorems all the steps except for the two marked Leibniz Law are references to theorems of the Toolkit and Z EVES can do simple equality reasoning So the proof can be presented to Z EVES as follows gt theorem example X Y Z VQ X Y R YZ S PVe QeoS sR Q3 S lt R proof use compldRight X Y R use compAssociates X Y Y use compldLeft
13. X C gt if A dj X B then A dj X BU X C A dj X C else A dj X BU X C We need to use the symmetry of disjointness again This suggests that making dj sSymmetric a rewrite rule might not have been a bad idea here it would have finished the proof automatically proof use dilsSymmetric X use dilsSymmetric X B C prove This turned out to be more work than the original line of argument A singleton set is disjoint from second set if its sole member is not in that set theorem rule djUnitLeft X Va X A PXe t dj ASGuraxceada The usual line of argument is successful 48 proof apply djDef prove a Subsets of disjoint sets are also disjoint theorem djMonotone X Z EVES Project TR 99 5493 06a VA A B B PX Adj BA A CAAB CBeA dj B We will start the proof of theorem djMonotone in the usual way applying the defining axiom for _ dj and running the prove command This gives the new goal AcEPX AA PX ABEPX ABE AA ABE PX PA ae A AN X B gt A n X B Sets can be shown equal by considering their members and the Toolkit contains at several different versions of the axiom of extensionality The theorem called extensionality is a disabled rewrite rule and can be applied to this goal to replace the two equalities This can be done by selecting New Command from the Edit menu entering the command apply extensionality s
14. Y Z prove a Q Z P Q Q id S Interestingly a final simplify command will not complete the proof because the instance of theorem compAssociates has the side condition id S Y gt Y which is not immediately obvious We could flesh out the proof with a detail of how to derive this but it is simpler to use the prove command and let Z EVES fill in the details itself Our next example is to prove that the domain and range a finite injection are of the same size theorem injSizeDomRan X Y Vg X Y e dom g ran g Recall that X Y is the set of finite injections that is finite one to one mappings from X to Y and X Y is the set of finite partial functions from X to Y Before starting an informal proof it is worth checking the Toolkit to see what is already known The section on finiteness contains something likely theorem axiom finiteFunction X Y fEexw VY gt domf e FX Aranf e F Y ran f lt dom f dom f f Using this fact we can argue as follows 1 Suppose g X Y 2 Then g X Y because injections are functions 3 Therefore by finiteFunction with f replaced by g we have domg FX A range FY A ran g lt domg lt 9 4 We also have g Y X because the inverse of an injection is a partial function 5 Therefore dom g lt rang by finiteFunction with X and Y interchanged and with f replaced by g Z EVES Project TR 99 5493 06a
15. a state that does not satisfy the predicate part of the state schema Clearly the circumstances under which this can occur are of some interest Z provides a reference to the precondition of an operation schema for a schema Op AS in IN out OUT the schema reference pre Op is equivalent to 35 out OUT e Op and describes the initial states for which an output and a final state are possible If the operation is total it can be executed in any starting state and with any inputs thus V S in IN e pre Op should be a theorem Trying to prove this conjecture can uncover any missing hypotheses A correct precondition theorem of the form VS in IN P e pre Op where P gives the precondition can be a useful form of documentation of a specification For example a Canadian City Hall marriage registry might contain a record of all married couples using a relation wife_of This relation is in fact a partial injection from men to women partial because not all men are married a function because a man may have at most one wife an injection because a woman may have at most one husband Registry wife_of Man gt Woman The Wedding operation adds new couple to the registry Wedding A Registry bride Woman groom Man wife_of wife_of U groom gt bride We can explore the precondition of this operation by adding a theorem paragraph theorem WeddingPrecondition V Registry bride
16. arithmetic facts e g Vz Ze x mazLength gt x or mazxLength maxLength gt 2 Forward rules As explained above a context is maintained during traversal This context is a set of predicates that are assumed true When a predicate is added to the context it may trigger a forward rule A forward rule is a theorem of the form P gt Q that has been labelled with the usage frule There are other restrictions on the form of such a rule see the Z EVES Reference Manual for details If an instance of P is added to the context the forward rule fires and the corresponding instance of Q is also added When a schema is declared a forward rule is automatically generated For the schema S z y Z lt lt y this rule is S gt x Z Ay Z Thus whenever S is assumed the types of its 42 Z EVES Project TR 99 5493 06a components z and y are known For the schema T S S this forward rule is T gt S AS Thus whenever T is assumed so are S and S this then triggers the forward rule for S twice to add information about x y z and y The syntactic restrictions on forward rules make them somewhat limited in their usefulness The most common use for forward rules is to forward chain from schema references to add equalities or inequalities to the context For example suppose we have the schema ResourceManager owner Resource User in_use P Resource in_use dom owner A typical operatio
17. be carefully distinguished e The infix union function U is slightly smaller than the generalized union function J e The infix intersection function N is slightly smaller than the generalized intersection function Q e The sequence concatenation function is different from the caret which is not used in Z e The schema operator is different from the semicolon which separates declarations and is relational composition 2 2 6 The Clipboard window The Clipboard window shows the contents of the Z EVES clipboard which is set by a Cut or Copy operation and used by a Paste operation The clipboard contents can be edited the editor is the same as used in the Edit window The clipboard window has the same appearance as the Edit window Z EVES Project TR 99 5493 06a 9 2 3 Composing and Checking a Specification We will use a small example a logging system adapted from Exercise 6 2 in Potter Sinclair and Till s book 9 to illustrate the use of Z EVES For the sake of brevity we will use only the first few paragraphs of that specification User Word LogSys password User Word reg active P User active C reg dom password InitLogS ys LogSys password active reg 0 Register A LogSys u User p Word password password U u gt p active active LogIn ALogSys u User p Word u active p passwo
18. details This is described in Chapter 5 4 1 Basic Concepts of the Prover 4 1 1 Logic Z EVES translates Z specifications into untyped first order predicate calculus which is the most familiar and well studied logical system All logical manipulations act on this translation Some restrictions are imposed on these operations to ensure that the result can be translated back into Z In some sense then Z EVES does not have a logic for Z certainly we cannot write all of the Z EVES manipulations in Z In a practical sense however Z EVES does have such a logic at the user level logical manipulations seem to be applied to Z predicates Because the underlying logic is untyped and because of the nature of types in Z information about the types of expressions is expressed and manipulated logically using set membership For 1 Actually we translate to a slight variant of classical predicate calculus that provides conditionals and does not distinguish predicates from expressions 2Very occasionally the result cannot be translated back Usually a subsequent rewrite or prove command corrects the problem 35 36 Z EVES Project TR 99 5493 06a example the fact that i is an integer is expressed by the predicate i Z Z EVES has no special deductive mechanism for type information its normal rules for predicates are used Types appear in a variety of side conditions and sneak into proofs through their appearance in generic actuals Whil
19. effective use of the prover it is necessary to learn the syntax of commands and to use one of the other two techniques to add them to a script When a proof command is running most Z EVES functions are disabled However it is still possible to select different windows and to scroll them A long running proof command can be stopped by selecting the Abort button Z EVES Project TR 99 5493 06a 7 2 2 3 The Theorems window Window Theorems Theorem definition IX CaninitLogSys i DeltasLoySyssdectaration theorem axiom CaninitLogSys InitLogSys declarationPart ALogsys InitLogSys LogingdeclarationPart Login domainCheck LogSys declarationPart Register declarationPart The Theorems window has two main parts On the left is a list of theorem names Double clicking on one of these names causes the theorem to be displayed in the right part of the Theorem window As for checked paragraphs in the Specification window the phrase structure of the displayed theorem can be explored Theorems correspond to theorem paragraphs in a specification or are generated when a paragraph is checked Generated theorems can be axioms which are facts that may be useful in later proofs or goals that are in need of proof These goals are either explicit theorem paragraphs or domain checks generated as described in Section 3 1 2 2 2 4 The Proof Scripts window The Proof Scripts window contains a list of proof scripts associat
20. models There are two different types of inconsistency which we call global inconsistency and local inconsistency Of the two global inconsistency is the more serious as it renders an entire specification unsatisfiable Global inconsistency An entire specification can be inconsistent if some axiom box generic box or predicate is too strong For example any specification containing the paragraph n Z n n has no models as there is no possible value for n In this case the inconsistency is obvious but in general it can be less so For example there is no function f satisfying the following description f N N Vn n Nen lt n ef n gt f n An inconsistency can also arise between different paragraphs in a specification each of which on its own is consistent Z EVES does not provide any specific mechanism for detecting such inconsistencies but has general mechanisms that can be used to detect them For example an axiomatic box gt can be checked for inconsistency by preceding it with the conjecture 4D e P For example proving 3 mazLength N e marLength gt 80 demonstrates that the axiomatic box maxLength N maxLength gt 80 Z EVES Project TR 99 5493 06a 23 is satisfiable Unfortunately it is not always easy to prove such conjectures to do so it is necessary to ex hibit suitable values for the declared names The Z notation does not always provide convenient expressions for this For example to
21. of Z EVES Project TR 99 5493 06a 25 the specification or of the specified system to be explored Z EVES supports several different types of exploration which are described in the sections below 3 2 1 Schema expansion The schema calculus provides a facility for the compact expression of models Sometimes though these representations may be too compact to be easily read Browsers can help by making it easy to find the definitions of any references in a schema box or schema expression Z EVES can help a reader by allowing a schema definition to be expanded and simplified The Z EVES schema expansion facility uses the prover and treats a schema as a predicate The invoke command can be used to expand one or more references in the predicate and the other proof commands can be used to simplify the results of the expansion For example consider the bank specification developed in Chapter 2 There we defined a schema NewAccount ABank users P Client id ID id accounts 3 Account OpenAccount e account account O id gt Account which refers to schemas ABank Account and OpenAccount We can begin a proof attempt with schema NewAccount used as a predicate by adding a paragraph theorem NewAccountExploration NewAccount and checking it This gives a new goal Selecting the proof for this paragraph e g by right clicking on the theorem in the specification window and selecting Show proof
22. the Toolkit but deserves special emphasis 6 3 A Theory Development Example One way to develop a theory is to be guided by the needs of its users identifying where support is needed from attempts to prove theorems involving the new concepts We will illustrate this approach using the concept of disjoint sets x _dj_ PX oPX VA B PXeAdjBSANB OH The logical adequacy of this definition is obvious the predicate determines the truth of A dj B for every pair A B in the domain of the disjointness relation We will use this concept in the specification of a simple resource management system This gives us several simple conjectures involving disjointness that are used to analyse the specification 6 3 1 A resource manager We will first present the specification of the resource manager and state a few conjectures Later sections will show the proofs The exact nature of these resources is immaterial we just use a given set Resources Resource The system records which resources are in use and which are available Manager used free P Resource used dj free Initially there are no used or free resources InitManager Manager used free 2The exception is a section that does not have the Toolkit as a parent 60 Z EVES Project TR 99 5493 06a As explained in Section 3 1 3 it is useful to ensure that this initial state is satisfiable theorem InitManagerlsOK 3 Manager e In
23. ways In this chapter we will describe two styles of using the prover explorative and planned In an explorative proof a user begins with some goal to prove and does not necessarily know a proof Various prover commands can be used to explore the proof space and with some luck the goal can be proved In this mode the user hopes to make maximum use of the automatic facilities of the prover In a planned proof a user spends some time working out an informal proof of the goal before starting to work on the proof in Z EVES As we describe below an informal proof can usually be used to guide a Z EVES proof session Which of these two modes is used is a matter of personal choice Explorative proofs are often successful for simple goals and we often begin a proof session with a brief period of exploration If that does not look promising rather than continuing to explore we stop to think about the goal and sketch an informal proof This informal proof may have fairly large gaps however which become new proof goals We often deal with these exploratively and so our Z EVES session is an intermixing of the two modes of proof 5 1 Explorative Proving In explorative proving the user tries to take maximum advantage of the automatic features of Z EVES and issues proof commands without necessarily having a clear idea of what the result will be or what the main line of proof is Generally the highest level of automation is provided by the prove o
24. 3 2 5 Test cases Many specifications are expressed in a form that makes them amenable to symbolic evaluation In particular if an operation defines the outputs and final state variables as functions of the inputs and initial state variables then it can be symbolically evaluated In such cases Z EVES can be used to investigate the results of sequences of operations by defining a test case schema as a composition of individual operations For example consider the following trivial bank account system with state that records an account balance _ Account balance Z an initializer that zeros the balance OpenAccount Account balance 0 and operations to deposit and withdraw funds 32 Z EVES Project TR 99 5493 06a Deposit A Account amount N balance balance amount _ Withdraw A Account amount N balance balance amount We can use sequential composition of schemas to define some test scenarios Testl OpenAccount Deposit amount 100 Test2 Testl g Withdraw amount 50 Test3 OpenAccount g Deposit amount 1000 3 Deposit lamount 20 3 Withdraw amount 500 Here we have used a Z EVES syntax extension schema replacement to set the values of the inputs to the operations This extension is not strictly necessary for example Deposit amount 100 could be written in Standard Z as J3 amount Z amount 100 e Deposit or as
25. 51 6 Since rang lt domg by step 3 and domg lt rang by step 5 we have dom g ran y There are just three steps in this argument that need further justification eygEXwY gt gE X Y Z EVES can make this inference automatically in a prove step So we do not need to make a lemma for this line e gE X Ysq Y X which we will state as a lemma and e the arithmetic reasoning in the conclusion which Z EVES can complete automatically Therefore we state an auxiliary lemma theorem step4Lemma X Y Vg X Yog e Y Y Now the main theorem can be proved following the argument outlined above theorem injSizeDomRan X Y Vg X Y e dom g ran y proof use finiteFunction X Y f gl use stepdLemmal X Y use finiteFunction Y X f prove a g X Y The lemma still needs to be proved but we will not show that proof here A more complex informal proof uses quantifier reasoning For example in trying to prove a universally quantified conclusion it is common to eliminate the quantifier stating something like let x be arbitrary Alternatively having proved an existentially quantified predicate of the form da X e P x it is common to again let z X P x be given and assume P x Both these steps can be presented to Z EVES as a prenex operation using the prenex command Existentially quantified conclusions are proved by proving some instance such an instance can be pr
26. Syntax and type errors The Z language has quite a complex syntax and the Mathematical Toolkit contains dozens of functions It is easy especially for an inexperienced Z user to make a mistake Z EVES like most Z tools detects and reports such type errors Unlike many other tools however Z EVES can be used incrementally as each paragraph of a specification is written it can be immediately checked and if necessary corrected DataBase data Key Data 19 20 Z EVES Project TR 99 5493 06a DeleteRecord A DataBase k Key data k lt data When schema DeleteRecord is checked an error is detected and the Syntax status column shows that there is an error Selecting Show errors from the pop up menu for the paragraph displays the following message Error FunctionArgType line 2 Type checker in application of global _ lt _ argument 1 has the wrong type Unfortunately the line numbers in error messages are not useful in any case we plan to replace the line number with an exact location marked in the given paragraph This message shows that the error concerns the type of the first argument of lt The prefix global indicates that lt is a global constant it is not logically necessary here but may sometimes help reveal how Z EVES has interpreted its input 3 1 2 Domain errors The Z notation allows one to write expressions that are not meaningful There are two ways to do so
27. T 1This case is debatable there is not yet complete agreement among Z authorities about the correct generic actuals to associate with the type of generic formal parameters The approach taken in Z EVES is to use generic formal parameters as though they are maximal Thus for example in the definition n X X U X the generic actual inferred for U is simply X Z EVES Project TR 99 5493 06a 59 where in the third rule we chose the opposite direction of rewriting than that suggested by the push in strategy then there is a possibility of conflict between the rules For example if a term of the form AN B is rewritten it is transformed by rule complementCap to A U B This can be rewritten by rule complementSetminus to AX B Rule diffSetminus then applies to the parenthesised term resulting in AN B which is exactly where we started Such rule loops should be avoided 7 Work with the Toolkit The Z EVES Mathematical Toolkit 10 contains many facts about the concepts introduced in the standard Z Mathematical Toolkit and most of these facts are expressed as rewrite rules Any rules added in a theory need to work together with these existing rules For example to avoid an ordering conflict with rule emptyDefinition a rule s pattern should contain instead of 0 8 Add assumption rules grules for abbreviation definitions as directed by the Z EVES Refer ence Manual This is really part of working with
28. The Z EVES 2 0 User s Guide TR 99 5493 06a Mark Saaltink Release date October 1999 ORA Canada One Nicholas Street Suite 1208 Ottawa Ontario KIN 7B7 CANADA Contents 1 Introduction 1 2 Using Z EVES 3 21 Running Z EVES e e eae ke YU eee BE eR Sa a eR ay 3 22 ZJ EVES Displays 4 434 604 8444 ee ee deb Add ewe has pt 3 2 2 1 The Specification window o 3 212 2 Phe POOF window ou aa hth RR ed ke ee A A 5 2 2 3 The Theorems window 0 0 0 ee 7 2 2 4 The Proof Scripts window ee ee 7 2 2 5 The Edit Window s est eai 822344554 aaa 7 2 2 6 The Clipboard window 0 0000 ee 8 2 3 Composing and Checking a Specification 2 ee 9 2 4 Analysing a Specification ee 14 2 5 APX Markip e OS eee AS eae ee ee pee eee ed 17 3 Analysing Z Specifications 19 3 1 Checking for Errors 4 a a da A ey A A 19 3 1 1 Syntax nd tyDeierTOLS 4 s s 4 eee daa e e a a ee 19 321 2 WDOMAIMETLOLSs taa a AS De de da ds BH eB ELS 20 3 3 INCONSIST NCY os 2A AS a a a A ee a 22 3 2 Exploring a Specification 2 24 3 21 Schema expansion cols 2244 pee eee eee eee ee ead 25 3 22 Preconditions 3 4 54 2 4444 0 22 de8 be hee ddhdie mada dd a s 25 3 23 Varias o 2 ck or arate te td bated ROA A ee ge ae Ss 27 IZA REO ment IBA AN anger e tr e AAA h 28 3 2 0 Testcases a Ad aE aS 31 3 2 6 Test theorems il AAA ee ee ee ead 32 4 The Z EVES Prover 35 4 1 Basic Concep
29. al forms menu in the Proof window The extra power that normalization gives Z EVES is especially noticeable when for example a hypothesis of the current goal is a disjunction or an implication Sometimes the rearrange command can be used instead of normalization rearrangement puts simple parts of a formula ahead of complex ones and tends to move nested Boolean connectives to the end of the conjunction or disjunction containing them The rearrange command appears in the Normal forms menu in the Proof window 4 2 2 Simplification In simplification Z EVES performs equality and integer reasoning propositional reasoning and tautology checking and applies forward rules and assumption rules where possible Propositional logic The rules of propositional logic e g the rules for the basic logical connectives are encoded in the traversal normalization and Boolean simplification mechanisms As a predicate is read and its parts considered the context of assumptions available at each part is determined by the propositional rules During simplification if a predicate is considered and it has already been assumed in the context it is replaced by true If it has been assumed false in the context it is replaced by false If a Boolean combination of predicates is considered and some parts are true or false the parts can be deleted if they are redundant e g 1 1 A true can be replaced by x 1 or the Boolean combination can be re
30. al part of a specification That is Z paragraphs are shown but no additional commentary or narrative text Text can be composed within Z EVES but can also be composed externally and imported in to it Eventually we intend to support a direct linkage with word processors at the moment only ASCII files marked up in PTFX can be imported see Section 2 5 4 Z EVES Project TR 99 5493 06a File Edit Command Window Eager E Syntax Proof Specification Al lt x User Word N N Logsys password User gt Word reg active User active C reg dompassword 12 InitLogSys Logsys password reg active ldo lt P lt Piy The status of each paragraph is shown in two columns to the left of the paragraph The leftmost column shows one of three symbols e indicates that the paragraph has not been checked e Y indicates that the paragraph has been checked and has no syntax or type errors e N indicates that the paragraph has been checked and has errors The next column shows the proof status for the paragraph using one of three symbols e indicates that the paragraph has not been successfully checked so proof status cannot be determined e N indicates that the paragraph has an associated goal that is unproven e Y indicates that the paragraph has no unproved goals Paragraphs can be added in several ways
31. any specifications need to introduce new concepts When some new name is introduced one or more theorems are added usually in the axiom of generic box introducing the name but sometimes as separate theorem or predicate paragraphs This collection of theorems forms the theory of the new name In order to be successful in getting proofs through Z EVES it is necessary to have a sufficient stock of theorems Numerous simple facts are needed in even the easiest of proofs and the power of the reduction commands depends critically on the available theorems The Toolkit defines a fairly rich set of theorems about its functions so that rewriting and reduction can automatically prove many simple facts When a specification introduces new functions the automatic commands will be unable to prove anything nontrivial unless some theorems about these functions are added Even worse proofs of simple facts involving references to the new functions might fail as well because some simple subgoal about the new function cannot be discharged In this chapter we will describe some of the approaches we use in developing a theory 6 1 Objectives The goal of theory development is threefold e logical adequacy The given theorems should determine the meaning of the new name e practical adequacy There should be enough support theorems about a concept to make it possible to prove typical theorems arising from the analysis of specifications using that co
32. base Personnel employees P PERSON boss_of PERSON PERSON salary PERSON N dom salary employees Ve employees e salary e lt salary boss_of e When schema Personnel is checked its status shows that it is syntactically and type correct but that it has an unproved goal Selecting Show Proof from the pop up menu shows the proof script for Personnel DomainCheck with the following goal predicate employees P PERSON A boss_of PERSON PERSON A salary PERSON N A dom salary employees A e employees gt e dom salary A e dom boss_of A boss_of e dom salary There are three conjuncts in the conclusion to prove corresponding to the three function appli cations in the last predicate of the schema We can simplify this predicate by using a rewrite or reduce command available in the Re duction menu in the Proof window The rewrite command produces employees P PERSON A boss_of PERSON PERSON A salary PERSON N A dom salary employees A e employees gt e dom boss_of A boss_of e dom salary One of the conjuncts e dom salary was eliminated but the other two remain There are several reasons in general why Z EVES might be unable to prove a predicate in this case these predicates are not true In fact these domain checking conditions show that we have forgotten some constraints in the schema Both conditions concern the well definedn
33. cate It is best to have some understanding of the general effects of these commands and how they use theorems before embarking on any difficult proof in Z EVES 4 2 1 Traversal and reduction Three reduction commands simplify rewrite and reduce traverse the goal predicate that is the predicate is examined in a left to right top to bottom reading Each part whether a predicate or expression is considered and possibly replaced by a new predicate or expression During the traversal Z EVES maintains a context which is a set of predicates that can be assumed true For example in traversing a predicate of the form PA Q R e first P is considered and possibly replaced by a new predicate P e with P assumed Q is considered and possibly replaced by a new predicate Q e with P and Q assumed R is considered and possibly replaced by a new predicate R e the result is in general P A Q gt R If one or more of the new predicates is true or false it can either be eliminated or the whole predicate replaced by true or false Predicates are added to the context during traversal in four ways e traversal adds it e an assumption rule adds it e a forward rule adds it or e the simplifier finds it to be true by equality chaining or by Boolean simplification 40 Z EVES Project TR 99 5493 06a The three reduction commands differ in the way they consider subformulas Each of the commands can a
34. corded as theorem rangeDef in the Toolkit As it is a disabled rewrite rule we can apply it The simplest way to do so is to select the expression 1 3 in the formula by clicking the left mouse button in it until it is fully highlighted then right clicking and looking at the choices in the Apply to expression submenu 4This is not true in two cases First a leading universal quantifier can be removed from a predicate giving a predicate that is not logically equivalent but which is a theorem if and only if the original goal is Second the cases command allows a conjunct or disjunct of a goal to become a new goal with the other parts temporarily hidden 38 Z EVES Project TR 99 5493 06a of the pop up menu Selecting rangeDef from this menu causes the prover rewrite with it replacing 1 3 by a set comprehensioin term and resulting in the new goal predicate 2 ifleZA3 Zthen k Z 1 lt kAk lt 3 elsel 3 The two side conditions did not appear in our informal proof We can eliminate them by simpli fication command Simplify from the Reduction menu 2 1k Z 1 lt kAk lt 3 The next step of our informal proof referred to set theory the rules of which are encoded by a large collection or rewrite rules in Z EVES and the Mathematical Toolkit The rewrite command would apply them here and complete the proof The trivial rewrite command in the Reduction menu applies just the most elementary rules
35. ct TR 99 5493 06a 15 vn lt gt sn Run Proof Script for CaninitLogSys Fr TE Reduction Cases Quantifiers Normal Forms Equality Formula ALogSys InitLogSys A gt Y The theorem s goal predicate is shown in the bottom half of the window An empty proof script occupies the top half As the proof of this theorem involves using the definitions of the schemas mentioned we can apply a powerful automatic proving capability by selecting Prove by reduce from the Reduction menu appearing in the middle bar of the Proof window This results in the following display vn fc gt gt sn Run Proof Script for CaninitLogSys Y prove by reduce action point AS Aaa Y Y Reduction Cases Quantifiers Normal Forms Equality Formula false _ 7 Y The proof script now contains the proof command we just selected the action point is after that step so the formula window shows the result of the step This result is the predicate false the conjecture is not after all a theorem We can return to the specification window by selecting Specification from the Window menu at the top of the Proof window Inspection of schemas Logsys and InitLogSys shows the source of the 16 Z EVES Project TR 99 5493 06a problem we erroneously wrote active C reg instead of active C reg in schema Logsys This is easily repaired selecting sc
36. d we focus on the mechanics of using Z EVES and techniques for using Z EVES to analyse Z specifications This version of the user s guide describes the graphical user interface to Z EVES Users of the command line interface should consult the previous version 11 instead Detailed descriptions of the syntax used by Z EVES the proof commands and the handling of Z paragraphs can be found in the Z EVES Reference Manual 7 A detailed description of the Z EVES Mathematical Toolkit appears as a separate report 10 Chapter 2 describes the mechanics of using Z EVES Chapter 3 describes several kinds of analysis that can be applied to expose errors in Z specifications or to explore the specification Chapter 4 describes the logical foundations and basic mechanisms of the Z EVES theorem prover Chapter 5 describes how to use the Z EVES prover The prover has an automatic mode which can prove many simple theorems When that fails however it is not always obvious how to proceed This chapter describes the strategies for successful application of the prover Chapter 6 describes how to define new concepts in a specification in a way that supports proofs Prover commands are shown in the text in typewriter font e g rewrite The terms user specifier and reader all refer to Z or Z EVES users Z EVES Project TR 99 5493 06a Chapter 2 Using Z EVES Z EVES is an interactive system for composing checking and analysing Z specificat
37. defining paragraph theorem axiom 4 X AECPXABEPX Adj X B 6 AN X B 0 X As we will see it is possible to attach a chosen name to this theorem by labelling the predicate We can appeal to a suitable instance of this fact and see where that gets us Z EVES Project TR 99 5493 06a 61 proof use aziom 4 Resource A B Z EVES rejects this command We will leave this unfinished and move on to the next theorem AddResourcelsHonest The command prove by reduce results in a goal used P Resource A free P Resource A r Resource A used dj free A r free Anr used gt used dj free U r We can use axiom 4 to eliminate the two instances of _ dj _ proof use ariomS4 Resource A used B free use axiom 4 Resource A used B free U r y prove a which results in the goal used P Resource A free P Resource A r Resource A used dj free Mar E free Nr used A used dj free U r gt used N free U r A free N used gt used N free U r This looks pretty messy and seem to have little to do with our original problem of the resource manager We will turn to the third goal AllocIsHonest Command prove by reduce produces the goal used P Resource A free P Resource A used dj free An free gt dr Resource e r free A used U r dj free r Since free is nonempty it has a member which could be
38. dit menu type in the command instantiate n k select Z EVES Project TR 99 5493 06a 39 Done from the File menu in the editor then run the command from the proof script window by double clicking on it This gives the new goal predicate keZAk gt 0 A KENA k kVk lt 1Ak lt l gt dn Nek nVk lt 1lAn lt l Instantiation is a bit odd in Z EVES instantiating x to e turns a predicate Jx S e P x into ee S A P s Viz S e P x This form is chosen to preserve the equivalence of the final goal with the initial goal Z EVES then converted the propositional form P gt QV Rto PAA Q gt R there are a number of such propositional rearrangements applied automatically In this case the resulting goal really is simple and Z EVES can look after the few details The prove or rewrite command results in a goal predicate of true and the proof is complete There is a strong benefit to the way proof steps preserve the meaning of the goal predicate Frequently a conjecture is incorrect and with luck after some number of proof steps it is trans formed into an obviously unprovable predicate e g n gt 0 Any counterexample e g 0 is also a counterexample to the original conjecture The preservation of meaning also allows proof steps to be used for various kinds of analysis of the specification as described in Chapter 3 4 2 Automation Z EVES has a number of automatic commands which can drastically change the goal predi
39. e Z allows the generic actual parameters in a global reference to be omitted e g users write NUN or 1 10 the semantics of Z rely on the presence of these actuals and Z tools infer suitable actuals when users omit them For example N U N represents the fully explicit term _U_ Z N N While these generic parameters are normally uninteresting a sound proof system for Z must take them into account it is easy to produce a proof of false in a system that ignores implicit generic actuals Z EVES follows common practice in omitting uninteresting generic actuals in its printed rep resentation of a formula however its internal representation maintains them and they sometimes resurface in side conditions For example the Z EVES Toolkit contains the theorem theorem disabled rule subDef X AEPXABEPX gt ACBS VWr AezecB Whenever we apply this theorem e g to Ni C N there is a side condition Ni PZ A N PZ The C in N C N has generic actual Z in the theorem it has generic actual X So X must be instantiated to Z to apply the theorem Generic actuals can play a surprising role in proofs sometimes making them more difficult than expected For example the predicate f A B gt domf A looks like it should make a useful theorem There is a problem though what are the generic actuals for dom Recall that we have dom X Y X gt Y PX If we use A and B then if we try to apply the theorem to say g
40. e asserting this theorem CanInitLogSys J LogSys e InitLogSys As for other paragraphs this can be added by selecting New Paragraph from the Edit menu clicking the mouse in the edit area when the Edit window appears and typing in the theorem using a combination of keystrokes and selections from the palette Fie Edit Enabled Disabled NONE theorem CaninitLogSys ALogSys InitLogSys Y css JJ JJ ower ld dae Box Drawing ele Eeee Subscripts CEE ETE fs JE Ee EA Toolkit Symbols efe ol cl clefofu o s of lt gt gt dole Bm sa Ja is JE JJ JE Jr Special Words it then else dom ran id seq iseg prefix suffix in disjoint partition bag inbag pre When Done is selected from the File menu this theorem is added to the specification and the specification window reappears When the theorem paragraph is checked the status bar shows it to be free of errors but not proved File Edit Command Window ebort Eager JEAN Syntax Proof Specification Y N ogin ALogSys u User p Word u active p password u password password active active u fu Y N theorem CanlnitLogSys ALogSys InitLogSys RRA o bA The proof can be started by selecting the theorem in the Specification window right clicking and selecting Show proof This exposes the Proof window Z EVES Proje
41. e will prove the more general fact VA PX e A dj This fact can be a rewrite rule and it looks like a good one the replacement in this case true is far simpler than the pattern A dj To make this a useful rewrite rule one other small detail needs to be observed The Toolkit rules replace by Thus it is better to use in the rule s pattern theorem rule djNullRight X VA PX e Adj The above rule is fine but it will not apply to a predicate of the form dj A which is also true In fact disjointness is a symmetric relation if A dj B then B dj A We can easily state and prove this fact but it is not so easily automated The equivalence A dj B B dj A can be made a rewrite rule Instead of leading to an infinite sequence of rewrite steps a rule like this is recognized by Z EVES and is treated specially Z EVES applies it at most once to a given instance and determines heuristically which permutation of the arguments is preferred However there is no guarantee that dj A would be permuted into A dj so that rule djNullRight would apply It seems we have no option but to state two versions of every interesting rewrite rule so that is what we will do theorem rule djNullLeft X VA PXe djA Although it does not help us in stating our main theorems here the symmetry of the disjointness relation is a useful fact theorem djlsSymmetric X VA B PXe Adj BSBdjA Our attempt to prove theorem AddResourcelsHonest w
42. ecked if the original paragraph had been checked Z EVES Project TR 99 5493 06a 5 A paragraph or group of paragraphs can be deleted by selecting it or them right clicking and selecting Delete from the pop up menu There is no undo capability in the interface so once deleted the paragraph cannot be recovered If a deleted paragraph had been checked all following paragraphs will become not checked A paragraph or group of paragraphs can be moved by selecting it them right clicking and selecting Move from the pop up menu This changes the mode of the interface As the mouse pointer moves over paragraphs they are darkened Selecting a paragraph causes the originally selected paragraph or paragraphs to be inserted immediately before the selected location The move can be canceled by right clicking then selecting Cancel from the pop up menu Paragraph order is important A Z specification is a sequence of paragraphs and requires dec laration before use The order in which paragraphs appear in the Specification window determines this declaration before use order Documents often present Z specifications with the paragraphs out of order if such a specification is imported into Z EVES it is necessary to move the paragraphs into a suitable checking order Order is also important for theorems as the proof of a given theorem can only use other theorems that precede the given theorem in the specification Thus lemmas mus
43. ed with the specification Each proof script is sequence of proof commands for a goal The script can be viewed in a Proof window by selecting the script s name right clicking and selecting View from the pop up menu Proof scripts are retained even when the associated goal disappears which can happen when a paragraph is deleted or becomes not checked The script is retained so that the proof can be reexecuted if the paragraph is checked again and the goal exists again A proof script is active if its goal exists Inactive scripts can be deleted by selecting the script s name right clicking and selecting Delete from the pop up menu 2 2 5 The Edit window The Edit window allows new paragraphs to be composed or existing paragraphs to be modified The editor provides standard editing capabilities such as insertion and deletion of characters cut and paste motion using cursor keys and mouse selection In addition it provides a palette of Z symbols below the edit area Clicking on a symbol inserts it into the edit area at at the insertion point where the cursor is 8 Z EVES Project TR 99 5493 06a File Edit Enabled Disabled NONE ogin ALogSys u User p Word u e active p password u nan nnna A se E aa 5 wom JEJ Efe EIEE EER E E E E E E E E Toolkit Symbols e o lt ON a ujale e o lt gt ajf e r o Maa ae AE Special Words ir then else dom ran a
44. eduction Cases Quantifiers Normal Forms Equality Formula ALogSys InitLogSys LE ASA Double clicking on the prove by reduce command in the script causes it to be run Now it results in the predicate true so the conjecture is indeed a theorem If we return to the Specification Z EVES Project TR 99 5493 06a 17 window by selecting Specification from the Window menu the status bar has been updated to show that the proof is complete File Edit Command Window Eager iy Syntax Proof Specification Al Y N Login ALogSys u User p Word u e active p password u password password active active u fi Y Y theorem CaninitLogSys ALogSys InitLogSys i PS Pl gt Chapter 3 describes the various analyses supported by Z EVES in more detail Chapter 4 describes the Z EVES prover Chapter 5 describes techniques for doing proofs 2 5 BTIT X Markup Z EVES can read a 4TRX markup representation of a Z specification so that files can be typeset as well as analysed The Z EVES distribution provides a package file called z eves sty that defines the necessary commands This file is compatible with AT X2e and can be applied to a document with the ATFX command usepackage z eves Aside from a small number of syntax extensions for Z EVES the markup macros defined by the z eves package are the same as those provided by Spivey
45. electing Done from the File menu then double clicking on this command in the proof script Alternatively for each equality it can be selected with the mouse then extensionality can be selected from the Apply to predicate submenu of the pop up menu exposed by right clicking In either case the result is AcEPX AA PX ABEPX ABE AA ABe PX PA ae A Yz AN X B ex A Vy feyEeAN X B gt Vx_0 A N X B e t_0 A Vy0 e y_0 4 N X B As usual in an exploration we immediately try the prove command and hope for the best In this case the result is AcCPX AA PX ABEPX ABE MA ABE PX PA PB Are A Ana Ae_0 AN X B e true gt x B Z EVES Project TR 99 5493 06a 49 Z EVES eliminated several quantifiers and simplified somewhat At this stage we need to think a bit We can argue as follows suppose x B held given the hypotheses of the goal Then we would have x A and x B as well because A C A and B C B This contradicts the hypothesis 320 AN X B e true We could proceed in several different ways Here we start with the hardest step for Z EVES dealing with quantifiers We argued that x is a witness value that contradicts the existentially quantified hypothesis so willtype in an instantiation command instantiate x__0 x execute it then clean up the formula as usual
46. em theorem rule decreasingReverse Vs seqZ s increasing e rev s decreasing This can be made into a rewrite rule so that if a predicate rev t decreasing is encountered for some sequence t Z EVES will consider the predicate t increasing If this subgoal can be proved the original predicate will be replaced by true But suppose Z EVES fails to prove the subgoal in some case where a user expected it to succeed In this case it is not so easy to find out what happened A stronger fact can be stated theorem rule strongDecreasingReverse Vs seqZ e rev s decreasing s increasing Now whenever a predicate rev t decreasing is encountered it is replaced with t increasing which might then be further rewritten or simplified 58 Z EVES Project TR 99 5493 06a This stronger rule has another advantage it can be used to refute predicates of the form rev s decreasing as well as to prove them For example the predicate x increasing A rev x decreasing can be reduced to false using the strong rule but is unaffected by the weak rule A simple fact about complementation is x E S gt x S This could be stated as a theorem but the equivalence VS PX a XerenSsr acres is stronger In fact and even stronger form is possible VS PXexe nS SerxrexArnzres This last form is useful in those hopefully rare cases where non maximal sets are used as generic actuals and allows us to show for exam
47. en t_O U 0 1 next A next gt 0 A 0 lt t_0 gt t_0 lt 1 next gt t U 0 1 next 0 next This is obvious but Z EVES is missing a trivial fact about ranges We can add the following lemma Z EVES Project TR 99 5493 06a 31 theorem rangeExtension Vajb Z a lt bea b a b 1 U b This is easily proved by extensionality after the commands apply extensionality and prove we are left with the predicate acz AbEZ Ma lt b A y bV a lt yAy lt 1 0b gt a lt yAySsb which Z EVES failed to prove automatically because it requires some consideration of cases Using any of the normalizing reduction commands i e with normalization simplify with normalization rewrite or with normalization reduce which can be found under the Normal Forms menu item in the proof commands menu bar is all that is needed to complete the proof With this lemma in place we can complete the refinement proof In the specification window the lemma s theorem paragraph must be moved to appear before theorem newAbs2 Then newAbs2 can be rechecked and its proof retried The prove by reduce command gives the same result as before we then use an instance of the lemma and let Z EVES finish the proof proof prove by reduce use rangeExtensionla 0 b next prove The interface offers no handy way to enter the use command It can be added by selecting New command from the Edit menu and typing it in
48. ess of the final condition in the schema Ve employees e salary e lt salary boss_of e The first e dom boss_of concerns the expression boss_of e In this context e is known only to be an employee However not every employee has a boss for example the president would not So this quantification should in fact range over only those employees having bosses A closer inspection of the schema shows that boss_of is some partial function with an unspecified domain This is probably a mistake bosses of non employees should probably not be recorded The second condition boss_of e dom salary concerns the expression salary boss_of e Does the boss have a salary This should be obviously true but it is not the specification says nothing 22 Z EVES Project TR 99 5493 06a about the range of function boss_of so a boss might not be an employee Again this was an oversight in the schema definition In the light of this analysis we can revise the definition to eliminate these flaws Personnel employees P PERSON boss_of PERSON PERSON salary PERSON N dom salary employees dom boss_of C employees ran boss_of C employees V e dom boss_of e salary e lt salary boss_of e This schema also has a nontrivial domain check condition but this time we can show it to be true 3 1 3 Inconsistency A specification is meant to be a model of some possible system A specification is inconsistent if it has no
49. ext Thus this lemma is 3For example after the declarations any X Fut if we ignore the missing generic actuals we can develop the predicate Y x y any x te x y in two ways first by observing that x t is always true if well typed hence the predicate is equivalent to V x y any e x y which is clearly false e g for x 0 and y 1 and second by observing that if x t holds and z and y have the same type then x and y are both in T are both equal to t and so are equal Therefore the predicate is true Z EVES Project TR 99 5493 06a 37 inserted into the specification at a point before where it is needed This insertion will cause any later paragraphs to become not checked Each specification starts in the context of the Mathematical Toolkit 10 There is at present no support for sections in the Z EVES interface Theorems can be stated explicitly in a specification by theorem paragraphs Theorems are also derived from the predicates in an axiom box or generic box Domain checking theorems can be generated for paragraphs Finally Z EVES may generate implicit theorems when a paragraph is added as explained in the Z EVES Reference Manual Every Z EVES theorem whether explicit or implicit has a name that can be used to refer to it in a proof step This name is provided as part of a theorem paragraph and can be attached to a predicate in an axiom box or generic box by means of a label which appears in c
50. f We might also have made a different lemma theorem thmla X Y VR X gt Yo ceerR gt i12 X y Yee z y which has a less trivial proof than the original form which adds a fact that is not immediately obvious to Z EVES and so which is not eliminated in a following prove step and which saves a step in the main proof This is easier to see in hindsight than when first planning the proof 54 Z EVES Project TR 99 5493 06a which can be cleaned up with the prove command The resulting goal is REX Y ALEX Aye Y e x y A z y ER gt z dom X YIRA y ran X Y R Z EVES has jumped ahead a bit in the argument applying the argument of step 8 but has left us with the remaining two interesting steps We bring in the two lemmas defined for these steps and clean up with a prove command proof use thm2 X Y use thm3 X Y prove and the proof is complete We are however not done We stated and used three lemmas now we need to prove them These proofs are relatively straightforward using a proof exploration and so are not discussed here Theorem thm1 can be proved by a prove command Theorem thm2 requires a few detailed steps proof with enabled inDom rewrite instantiate y 0 y prove use thm1 X Ylle z y prove Theorem thm3 can be proved by using theorem thm2 on the inverse relation proof use thm2 Y X R RY X Yl z y y z prove a Chapter 6 Theory Development M
51. f is not complete we are left with the goal AEPXABEPXACEPX gt if AN X C then CN z AU 1 B Ss BnN X C else gt CN X AU X B We can try some algebraic reasoning here using the fact CN AUB CN A U CNB followed by the observation that a union of two sets is empty if and only if the two sets are themselves both empty We could look for this theorem in the Toolkit documentation or alternatively can select the subexpression C N z A U z B right click and look through the Apply to expression submenu The very first choice is a theorem called distributeCapOverCupRight Selecting this causes both occurrences of the selected subexpression to be rewritten Running a prove command to clean up the formula in fact completes the proof the goal is now true We are in luck the fact about empty unions was applied automatically by the prove command Theprevious theorem has a symmetric counterpart with the union in the left argument of dj rather than the right theorem rule djCupRight X VA B C PXeAdj BUCSAdBAAdjC We could prove this theorem in the same way we proved djCupLeft but probably using a different distribution law Instead here we will try a different line appealing to to symmetry of disjointness and using djCupLeft proof use djIsSymmetric X B B U X C prove a This results in the goal AEPX ABEPX ACEPX A if B dj X A then A dj X B U X C C dj X A else A dj X BU
52. for AllocIsHonest is not much different from the previous attempt the appeals to axiom 4 are gone but nothing else has changed This approach has not been a big improvement We could follow two paths One is to stick with the elimination idea and prove some additional facts about intersection so that the above proofs can be completed more easily The second path which we explore in the next section is to abandon the elimination approach and add some useful facts about disjointness 6 3 4 Third attempt developing a theory Eliminating occurrences of _ dj was not a completely successful approach There is a further drawback we defined this notion as a convenient and useful concept for use the specification So it is rather annoying to have it eliminated in proofs In this attempt we will not eliminate the disjointness relation from theorems instead we will prove a number of simple facts about disjointness We can be guided in our selection of theorems by our previous proof attempts We first redefine disjointness this time making the defining predicate a disabled rewrite rule This lets us rewrite with it when we choose to eliminate disjointness as will be necessary in several proofs below x _dj_ PX oPX disabled rule djDef VA B PXeAdj BS ANB 9 64 Z EVES Project TR 99 5493 06a From the proof of theorem InitSIsOK we know that the fact dj is needed In fact any set is disjoint from the empty set so w
53. hema LogSys in the Specification window right clicking and selecting Edit from the pop up menu exposes the Edit window with the LogSys schema in it The correction is easily made When Done is selected from the File menu we are returned to the Specification window which now has the following appearance File Edit Command Window ebort Eager JEAN Syntax Proof Specification y Y User Word gSys password User gt Word reg active P User active Creg dompassword InitLogSys LogSys password reg active AAA A Y As the status bars show the revised version of LogSys is not checked Furthermore all the following paragraphs are not checked either Since the modification to LogSys might have changed the schema s type all these paragraphs need to be rechecked with respect to the new definition These paragraphs can be checked one by one by couble clicking on them on at a time Alternatively Check all paragraphs can be selected from the Commands menu this will check all the unchecked paragraphs There are no syntax or type errors We can revisit the proof of theorem CanInitLogSys by right clicking on it and selecting Show proof from the pop up menu The old proof commands are retained but have not yet been executed Run Proof Script for CaninitLogSys action point prove by reduce i y Y R
54. hevrons before the predicate e g cNonnegative c gt 0 If no name is given Z EVES assigns a name Implicit theorems always have names assigned by Z EVES 4 1 3 Proof style Z EVES gives a somewhat unusual style of proof A proof applies to a goal predicate which is manipulated by proof commands Proof commands when they succeed result in a new goal predicate which is equivalent to the original When the goal has been transformed to true the proof is complete Such a proof can be presented informally as a chain of equivalences For example 2 1 3 lt definition of _ _ 2 flr Z 1 lt x lt 3 4 set theory da Z 1 lt a lt 3er 2 lt gt one point rule 2EZA1 lt 2 lt 3 arithmetic true In this informal proof we have given a hint for every step in the chain In developing a proof with Z EVES we use proof commands to transform each predicate to the next It is possible to follow this proof plan in Z EVES but we seldom want to work at this level of small details Indeed the rewrite reduce and prove commands each complete this proof in a single step For illustration here is the detailed proof in Z EVES We begin the proof by adding a theorem with the New Paragraph function in the Edit menu theorem SimpleTheorem 2 1 3 checking it then selecting it in the Specification window right clicking and selecting Show proof from the pop up menu The definition of _ _ referred to above is re
55. ill not show here The reduce command then results in the predicate wife_of Man Woman A bride Woman A groom Man gt groom dom wife_of wife_of groom bride A bride ran wife_of gt wife_of bride groom which expresses rather concisely the precondition if the groom is previously married then the bride must be his wife and similarly if the bride is already married then the groom must be her husband We can go back to the Specification window to revise the theorem to its correct form making the actual precondition apparent theorem WeddingPrecondition V Registry bride Woman groom Man bride ran wife_of A groom dom wife_of e pre Wedding This can be rechecked and reproved The commands used in the exploration are still in the proof script and can be rerun by double clicking them in sequence to complete the proof 3 2 3 Invariants Given a sequential system defined with an initialization schema nit and a collection Op Opn of operations a predicate J is an invariant if Init gt I and for every i 1 k I is preserved by the ith operation that is we have I A Op I Such invariants can be important for a variety of reasons e An implementor can take advantage of an invariant to simplify an implementation If for example x y z is an invariant then one of xz y or z may be computed as needed rather than stored explicitly in the state If some sequence i
56. iom is disabled as we do not normally want Z EVES to expand out the concept of disjointness but is a rule as rewriting is the most convenient way to use a theorem like this theorem rule djNullRight X VA PX e Adj In trying this proof a prove or prove by reduce command does nothing Of course we need to use the definition of relation _ dj _ as expressed by theorem djDef As that is a disabled rule we can apply it There are two ways to do so compose a new proof command apply djDef in the editor and add it to the proof script or select the expression A dj X in the goal predicate right click and select djDef from the Apply to expression submenu of the pop up menu In either case we get the new goal AcPX gt if AEPXA eEPX then AN X O X else A dj X Now we will use the prove command to clean this up and see what results In this case prove results in true and our proof is complete The next theorem shows that disjointness is a symmetric relation theorem djlsSymmetric X VA B PX eAdj BeBdjA The symmetry of disjointness similarly needs to use the definition of _ dj _ and is otherwise trivial proof apply djDef prove A set is disjoint from a union only if it is disjoint from the two summands theorem rule djCupLeft X VA B C PXeAUBAGCSAAGCABGC We will begin the proof with our usual line of attack proof apply djDef prove Z EVES Project TR 99 5493 06a 47 This time the proo
57. ion Of the two systems forward simulation is the most commonly used Given an abstract system with state A initialization schema AJ and operation AO and given a similar concrete system with state C initialization schema CT and operation CO we can demonstrate a forward simulation by exhibiting some relation R between the abstract and concrete states proving the initialization theorem VCIeJAleR and proving two theorems for the operation Firstly VR pre AO e pre CO shows that the concrete operation can be invoked whenever the abstract operation can Secondly VR CO pre AO e JA e AOAR shows that when the abstract operation can be invoked it can give a result consistent with the concrete operation There are several equivalent ways to express these relations the presentation here differs from Woodcock and Davies in form but not in meaning For example here is a definition of a trivial system that dispenses numbered tickets so that a different number is issued on every call The state thus has a component that records the numbers that have been issued TicketA given PZ Initially no tickets have been issued InitA TicketA given A new ticket may be requested the resulting number has not previously been issued and is recorded in the set of issued tickets NewA A Ticket A tl Z t given given given U t That ends the abstract descriptio
58. ions Speci fications can be entered and checked one paragraph at a time checked paragraphs can be revised and rechecked and theorems can be stated and proofs attempted at any time Z EVES is also able to read entire files of specifications that have been previously prepared using 4T X markup This chapter describes the mechanics of using Z EVES 2 1 Running Z EVES Z EVES is run on a Unix system by the command z eves if it has been installed correctly on Windows it is started by running a shortcut The installation guide describes how to install and run it Z EVES has two parts a server that checks paragraphs and executes proof commands and a graphical interface that manages specifications sends commands to the server and displays results In Windows the server displays a small window however it does not respond to user input or mouse clicks Usually one does not need to be aware of these two parts However if something goes wrong it may be necessary to terminate one or both of these processes 2 2 Z EVES Displays Z EVES has six main displays five of which can be selected under the Window menu in the menu bar The Edit window is instead exposed when edit commands are selected and disappears when editing is complete 2 2 1 The Specification window The Specification window is the main display and several important functions such as saving or exiting are only available from it The specification window shows the form
59. itManager The AddResource operation introduces a new resource which is initially available AddResource AManager r Resource r free U used used used free free U r As explained in Section 3 2 2 it is good to examine the precondition of the operation theorem AddResourcelsHonest V Manager r Resource r E free U used e pre AddResource The Alloc operation is used to obtain a resource Alloc A Manager r Resource r free free free r used used U r We will also examine the precondition of this operation theorem AllocIsHonest Y Manager free 4 e pre Alloc Obviously we need more operations to make a realistic specification however the three conjec tures above are all we need to illustrate the issues in theory development 6 3 2 A first proof attempt For our first attempt we will just roll up our sleeves and start proving All three theorems depend on the schema definitions so we begin the proofs with a prove by reduce command and see what happens For InitManagerIsOK prove by reduce results in the goal dj This is exactly the sort of trivial fact that Z EVES should be able to prove automatically For now we will forge on proving this fact by using the definition of _ dj _ When the definition was introduced Z EVES adds two theorems which can be seen in the Theorem window A theorem called axiom 4 contains the predicate from the
60. ithout eliminating the disjointness pred icate resulted in the goal used P Resource A free P Resource A r Resource A used dj free N r free Anr used gt used dj free U r Two general facts about disjointness are applicable here First a set is disjoint with the union of two others if and only if it is disjoint with each of the two other sets theorem rule djCupLeft X VA B C PXeAUBdGCSAAGCABGC This rewrite rule also needs a right hand variant theorem rule djCupRight X VA B C PXeAdj BUC SAGBAAQC Secondly a set A is disjoint with a unit set x if and only if x is not a member of A theorem rule djUnitLeft X Va X A PXe t dj AGuruxcead Z EVES Project TR 99 5493 06a 65 We again want a right hand variant theorem rule djUnitRight X Va X A PXeAdj r a ured Finally when we tried to prove AlloclsHonest we had the contradictory hypothesesused dj free and used dj free x That these are contradictory is a consequence of the general fact that subsets of disjoint sets are also disjoint theorem djMonotone X VA A B B PX Adj BA A CAAB C Be A dj B There seems to be no straightforward way to automate the use of this theorem so we leave it as a plain fact With these theorems in hand we can retry the three proofs Both InitManagerIsOK and AddResourcelsHonest are proved by the prove by reduce command For AllocIsHonest more work is required proof prove by red
61. mand is useful in proofs where it is necessary to appeal to the definitions of the terms involved It is very commonly used in proofs about schemas for example or about abbreviations In proofs about complex schemas or in theories with long chains of definitions reduction may be inadvisable as the goal will be reduced to primitive terms It is usually better to introduce enough theorems about the defined notions as described in Chapter 6 so that the notions can be kept in the goal This usually gives easier to read goals and more manageable proofs Definitions can be expanded selectively with the invoke command when it is appropriate to do so in a proof A defined name appearing in a goal predicate in the Formula part of the Proof window can be invoked by selecting it right clicking and selecting Expand this name from the pop up menu 4 2 5 Prove loops The prove and prove by reduce commands provide the highest level of proof automation These commands apply a commonly used combination of other commands until the proof is finished or no more progress is made The other commands used include prenex to eliminate quantifiers if possible rearrange to re order the predicate putting simpler hypotheses before complex ones equality substitution to use equality hypotheses and either rewrite for the prove command or reduce for the prove by reduce command Chapter 5 Proving Theorems Z EVES supports theorem proving in a variety of
62. mbine several paragraphs before showing consistency Situations involving given types are more complex Consider for example the given type Name and the assertion that Tom Dick and Harry are three distinct names Tom Dick Harry Name Tom Dick Harry 3 We cannot state the relevant consistency condition which would express the proposition that Name Tom Dick and Harry exist However given a set S that could be a suitable meaning for Name we can then express the proposition 24 Z EVES Project TR 99 5493 06a Tom Dick Harry S e Tom Dick Harry 3 which could be proved It is also possible for a free type definition to be inconsistent For example the definition BigSet make_set P BigSet has no models it specifies that BigSet is isomorphic to its powerset This is impossible as the powerset always has more elements Restrictions on free type definitions that guarantee consistency are described by Arthan 1 Smith 12 and Spivey Section 3 10 2 page 84 13 Z EVES does not provide any special facility for generating these conditions The reader might be wondering at this point if anything is safe Indeed some things are given set declarations abbreviations and schema definitions cannot introduce global inconsistency No theorem that has been proved in a globally inconsistent specification can be trusted as its proof is potentially based on impossible assumptions Local inconsistency
63. n of the ticket system A concrete implementation issues tickets in sequence beginning with 0 recording the next avail able number TicketC next N Initially the next available number is 0 30 Z EVES Project TR 99 5493 06a InitC TicketC next 0 When a ticket is requested the next available number is issued New A TicketC t Z t next next next 1 To show that the concrete system refines the abstract system we need the abstraction relation Here the set of given numbers is the range 0 next 1 TicketAbs TicketA TicketC given 0 neat 1 Now we can prove that corresponding operations are refinements For initialization we show theorem init Refinement V InitC e 3 InitA e TicketAbs which can be proved with a prove by reduce command Obviously reduce is needed here as the definitions of most of the schemas must be expanded in the proof For the New operation we have two things to show First the preconditions are suitably related theorem newAbsl V TicketAbs pre NewA e pre NewC This can also be proved with a prove by reduce command Second we need to show that the effects of the operations are related theorem newAbs2 V NewC TicketAbs pre NewA e 3 TicketA e NewA A TicketAbs This time the prove by reduce command results in next Z A next 1 next Atl next A given 0 1 next At0 leZ A giv
64. n schema might be Free A ResourceManager r Resource u User r in_use owner r u owner r lt owner and its domain checking condition is V AResourceManager r Resource u User e r in_use gt r dom owner This can of course be proved with the reduce or prove by reduce commands Sometimes however it is undesirable to invoke the ResourceManager schema In this simple example it does not matter much but if the schema definition and the domain condition were more complex the use of reduction would expand the formula too much In such a case it might be useful to add the forward rule theorem frule ResourceManagerFact ResourceManager gt in_use dom owner With this forward rule in place whenever a reference to schema Resource Manager is assumed the simplifier will also assume n_use dom owner Thus in the domain condition above by the time r dom owner is considered AResourceManager and r in_use have been assumed Z EVES automatically adds a forward rule for the above the line material in a schema so the assumption AResourceManager triggers the automatic rule and adds ResourceManager and ResourceManager Forward rule ResourceManager Fact is triggered by both these so in_use dom owner and in_use dom owner are added With all these facts in the context r dom owner is recognized as true Thus the domain check can be proved with the rewrite or pro
65. ncept e automation When practical there should be enough rewrite rules forward rules and assump tion rules so that trivial facts can be proved automatically 6 1 1 Logical adequacy A collection of theorems is logically adequate if it describes the new concept exactly There is no general way to test the adequacy of a set of theorems It is possible to test if the theorems determine exactly one concept For example given a definition f ZN Va Nef r 2x z Vi Z x lt 0ef x z 55 56 Z EVES Project TR 99 5493 06a we can try to prove df ZoNe Va Ne f s 2 2 A Vr Z 2 lt 00 f r 2z thus showing that the two constraints in the axiom box determine exactly one possible value for f However this still does not show that these constraints determine the right function the one the specifier had in mind Furthermore it is sometimes the case that a specifier intentionally leaves some cases unspecified For example the size of a hash table may be specified as some arbitrary large prime hashTableSize Prime hashTableSize gt 1000 In cases like this the reader needs to apply judgment in determining whether the specification is logically adequate 6 1 2 Practical adequacy A theory is practically adequate if it provides theorems that are convenient in proofs A theorem can be logically adequate and yet express its theorems in a way that is hard to use or that makes proofs of even simple facts difficult The
66. ng New Paragraph from the Edit menu again brings up the Edit window The easiest way to enter the schema is to select Schema Box from the Edit menu which draws the schema box outlines File Edit Enabled Disabled NENE eno a of ole al meo eS e e a lalala Box Drawing eee Subscripts ro fe E E JE E E ea Ee Toolkit Symbols efe a cl clefofu o s eleal e dole da 149150 Special Words if then else dom ran ia seq iseq prefix suffix in disjoint partition bag inbag pre We can then click in the top line type in the schema name LogSys click in the declaration part of the box and type in the declarations then click in the predicate part and type in the schema s constraints Special characters can be entered by clicking on them in the palette below the edit area The results including two typing mistakes included for illustrative purposes appear as follows 12 Z EVES Project TR 99 5493 06a as Enabled Disabled A LogSys __ _ A AqqqqqqAAAAAA n nzs A password User gt Word reg active User active C reg dom password a AAA Soe as as subsenpts EEE we eg ee et a es em ea ey REEERE CEREA pe ea ES E ca E Fla JJ EJ JE JNE sawe e a e pa 1 pa pra pa isis rota o is a Note that when a new line is started in the schema box the box is not drawn This does not matter the schema will be cor
67. nt proof There is an interesting case where it is not possible to add the invariant to the state schema Given a system with operations Opl Opn then if pre Op1 V V pre Opn is invariant the specified system never gets stuck in any reachable state some operation is always possible This desired invariant cannot be included in the state schema because it cannot be expressed until the operations have been defined and the operations cannot be defined until the state has been defined In this case therefore the kind of proof described in this section is applicable 3 2 4 Refinement Z is often used to describe abstract data types A state schema gives an abstract model of the set of values of the type an initialization schema describes the possible initial values and one or more operation schemas describe the operations on the type In these cases Z can also be used to express implementations of abstract data types by giving a second more concrete abstract data type and proving that a refinement relation holds between the two types The rules for proving a refinement are described in detail by Woodcock and Davies 15 who give two different sets of rules one 1This uses an interpretation of operation schemas that considers the precondition of a schema to be an enabling condition in which the operation is allowed to be invoked Z EVES Project TR 99 5493 06a 29 for forward simulation and the other for backward simulat
68. ntext Assumption rules During traversal any theorems labelled as grules assumption rules can be used As explained in the Z EVES Reference Manual an assumption rule has a trigger formula If during traversal an instance of a rule s trigger is considered the rule may be applied If the rule s predicate is not an implication it is added to the context If the predicate is conditional the hypotheses are looked up Tf the hypotheses are true the conclusion is added to the context A hypothesis is looked up by seeing if a contradiction results from assuming it to be false Assumption rules are frequently used to make the type of a global reference known or to add inequalities concerning integer global constants Consider for example the paragraph mazxLength Ny Z EVES automatically adds the assumption rule mazLength declaration asserting mazLength N This is useful in conjunction with the weakening rules in the Toolkit when rewriting allowing for example both mazrLength N and mazLength Z to be rewritten to true The simplifier however knows nothing about natural numbers and if we try to prove Vz Ze x mazxLength gt x we get nowhere We can add a grule that adds information about maxLength theorem grule maxLengthBound maxLength gt 1 Now whenever the prover encounters marLength it will add the fact mazLength gt 1 to the context With this extra fact the simplifier can prove simple
69. ot show the proofs here 66 Z EVES Project TR 99 5493 06a Bibliography 1 2 3 10 11 12 13 14 15 R D Arthan On free type definitions in Z In Nicholls 8 pages 40 58 R Barden S Stepney and D Cooper Z in Practice BCS Practitioner Series Prentice Hall 1994 Dan Craigen Irwin Meisels and Mark Saaltink Analysing Z Specifications with Z EVES In J P Bowen and M Hinchey eds Industrial Strength Formal Methods Springer Verlag FACIT series 1999 I J Hayes editor Specification Case Studies Prentice Hall International Series in Computer Science 2nd edition 1993 ISO Z notation Technical report ISO IEC JTC1 SC22 N1970 1995 ISO CD 13568 Com mittee Draft of the proposed Z Standard Jonathan Jacky The Way of Z Practical Programming with Formal Methods Cambridge Uni versity Press 1997 Irwin Meisels and Mark Saaltink The Z EVES Reference Manual Technical Report TR 99 5493 03d ORA Canada September 1997 J E Nicholls editor Z User Workshop York 1991 Workshops in Computing Springer Verlag 1992 B F Potter J E Sinclair and D Till An Introduction to Formal Specification and Z Prentice Hall International Series in Computer Science 2nd edition 1996 Mark Saaltink The Z EVES 2 0 Mathematical Toolkit Technical Report TR 99 5493 05b ORA Canada October 1999 Mark Saaltink The Z EVES User s Guide Technical Report TR 97 5493 06 ORA Canada Oc
70. ove might be defined even though it contains an expression that may be undefined So the proper treatment of undefinedness in Z is not clear In any case it is clear that normal mathematical reasoning is not always applicable For example the formula a a b is always true in normal set theory it can fail in Standard Z if say a is defined and 6 is undefined as then a b is also undefined The approach in Z EVES is to show that expressions are always meaningful The type system of Z is not strong enough to guarantee this so another kind of analysis is used Z EVES examines each paragraph as it is entered and checks each function application and definite description for meaningfulness Many applications are easily seen to be meaningful because the function applied is total over its type For example the application of _ _ to two arguments is always defined because type checking guarantees that the arguments are integers and the domain of addition is all pairs of integers In contrast an application of _div_ is not necessarily defined type checking does not show Z EVES Project TR 99 5493 06a 21 that the second argument is non zero When type checking does not guarantee meaningfulness a predicate called a domain check is generated If the domain check is true then the original expression is meaningful An example may help to clarify how domain checking works Consider the following schema intended to describe a simple personnel data
71. ovided in a Z EVES proof with the instantiate command For example we can show 3x S ex T S C T using the following argument 1 Assume Ja Sez T 2 Choose such an x so assume z S and z T 3 SCT sS Ve Sece T by theorem subDef 4 Putting e x shows S C T is false theorem example2 VS T PZe r Sexr T S73SCT The choice of x in step 2 can be presented as a prenex command which results in the goal SEPZATEPZALESAL amp ET gt ascT 52 Z EVES Project TR 99 5493 06a We can now bring in the instance of theorem subDef needed for step 3 with the command use subDef num A S B T This gives the goal SEPZATEPZS SCTS amp Vr_0 Sexr_0 T ASEPZ ATEPZ ATES ALT gt n SCT Theorem subDef actually uses x as its bound variable instead of the e we used in the informal proof sketch When the theorem is used Z EVES renames the bound variable to avoid conflict with the z aleady appearing in the goal So our subsequent instantiation needs to use the new name The command instantiate x__0 x can be followed by prove and the proof is complete In summary the proof script is proof prenez use subDef Z A S B T instantiate 10 2 prove A Our next example goal is to prove theorem relationInDomCrossRan X Y VR X YeRe domR gt ran R Informally we can argue as follows Suppose we are given R X gt Y We must show R dom R ran R Now 1 2
72. pend time working on a trivial fact about the basic concepts used A well automated theory allows Z EVES to prove these trivial facts by itself freeing the specifier to concentrate on the more interesting and illuminating aspects of the proof We certainly do not advise a huge investment in setting up a theory so that all the interesting proofs are fully automatic This is an ambitious undertaking and likely not worth the effort It is worthwhile however spending enough time to make the trivial steps automatic 6 2 Guidelines Several guidelines can be applied in the development of a theory We can illustrate some of them using the following definition of the complement of a set with respect to its type Z EVES Project TR 99 5493 06a 57 X PX PX VS PXe S X S 1 Use plain facts There can be a temptation to express properties in a compact form using various notions from the Toolkit A theory is more likely to be practically adequate if its facts are stated in a simple and direct form For example instead of a theorem asserting disjoint S S it is probably more useful to assert rE S gt gt xES 2 Look for rewrite rules Rewriting is by far the easiest of the prover s mechanisms to understand and control and many mathematical facts make natural rewrite rules if they are expressed properly Rewrite rules that help reduce the size and complexity of a goal are particularly valuable as are rules
73. placed by true or false e g gt 2 gt true can be replaced by true These two mechanisms traversal and Boolean simplifications allow the simplifier to recognize many tautologies For example simplification replaces the predicate x S gt x E S in two steps first the second occurrence of z S is replaced by true second x S gt true is replaced by true When normalization is used e g in the command with normalization simplify the sim plifier recognizes all tautologies Z EVES Project TR 99 5493 06a 41 Equality The simplifier has a decision procedure for the facts about equality including the substitution of equals for equals For example the predicates x 1 x Y y x and X Y gt PX P Y are all recognized as true Arithmetic Simple arithmetic facts are known to the simplifier For example simplification turns 1 lt 2 into true and 2 gt 3 4 into false The simplifier also deals with linear arithmetic involving addition negation or multiplication by a literal constant For example z gt 1 gt x gt 0 is recognized as true asareWVzx y 2 Zexr lt y lt z gt x lt zanmdVir y Z 1 lt xA2 3xx lt ye5 lt y More complex terms can appear in place of the variables in these examples so long as these terms are known to be integer A term t is known to be integer if the fact t Z is in the context As explained below it is sometimes useful to define assumption rules to add such facts to the co
74. ple S N given the definition S X S 4 PX 1 A In this case the generic actual for is N rather than the maximal set Z Even in those cases where the theorem is not suitable as a rewrite rule a strong form of the theorem can be more powerful and thus more useful than a weaker form Avoid complex conditions Generally it is advisable to ensure that any conditions or a rewrite rule are not more complex than the pattern In particular it is probably not a good idea to have a rule that introduces some new concept in its conditions For example a rule theorem rule largePrimesAreOdd Va Prime x gt 2ex Odd is silly any time a predicate n Odd is rewritten the primality of n will be considered This is likely to be a complete waste of time Make rules work together It is wise to have some overall strategy in mind when writing rewrite rules For example a good strategy for complementation might be to push complementation inside other set connectives that is to rewrite AU B to A N B and so on A collection of such rules expressing defines a kind of normal form for set expressions In the absence of a coherent strategy for the rules about complementation it is easy to run into trouble For example if we have the three rules theorem rule complementCap X VS T PXe SNT S U T theorem rule diffSetminus X VS T PXeS T SNT theorem rule complementSetminus X VS T PXe S UT S
75. pply certain theorems or definitions as explained in the detailed descriptions below The reduction commands use only theorems and definitions that are enabled The declaration of a name or theorem may specify that the name should normally be disabled A command modifier can be used to enable or disable a theorem or definition for a single reduction command see the Z EVES Reference Manual for details By default Z EVES retains the propositional structure of a predicate during traversal In some situations however consideration of cases is suggested For example in traversing the predicate PV Q A P gt R A Q gt R gt R the prover is unable to infer the conclusion R If normalization is used any time there is a Boolean connective nested inside another there is a consideration of cases So for example a predicate of the form P V Q A R is converted into if P then R else Q A R When the if form is traversed R is considered twice once with P assumed and once with P denied and Q assumed In the above example normalization gives a long formula where R can be inferred Thus normalization increases the power of the prover However since normalization involves repeating parts of a formula the current goal can become extremely large so it is disabled by default The with normalization command modifier enables normalization during performance of the specified command Prover comands with normalization are available in the Norm
76. practical adequacy of a theory is generally determined by doing proofs these will expose any weaknesses or awkward areas For example it is possible to define the concept of a partial function as X YV R XOY RY3RCidY This definition is certainly logically adequate for the definition of partial functions However this definition is not necessarily the most convenient for use in showing that a particular relation is a function The usual line of argument in showing that a relation Q is a function is to show Va X y y Y 2 y E QA z y E Qe y y It is possible to get a subgoal of this form from the above definition of partial function but it is not particularly easy So a theory of partial functions consisting of just the above definition is not practically adequate Either some other definition should be used or even better additional theorems should be given so that a specifier has a choice of different ways to prove that a relation is a theorem 6 1 3 Automation A good collection of rewrite rules forward rules and assumption rules for a basic theory makes it easier to prove theorems involving its concepts New notions are introduced because they are needed in a specification and these notions will appear in the theorems generated while analysing the specification While proving a domain con dition the satisfiability of some schema or some other fact about a specification it can be an annoyance and a distraction to s
77. r prove by reduce com mands Of the two prove is less powerful but generally faster as it does not expand names defined as abbreviations or schema references Many simple theorems are proved automatically by prove If a prove command gets off track it is often possible to use some combination of the commands reduce rewrite simplify rearrange prenex and equality substitute to proceed in the proof or to bring in some theorem with a use or apply command Except for the last two these commands are available from menus in the Proof window Candidates for the apply command can be found by selecting a predicate or expression in the goal right clicking and expanding the Apply to expression or Apply to predicate submenu of the pop up menu this shows the disabled rewrite rules that apply to the selected formulas Here are some examples of explorative proofs of some theorems about disjoint sets These theorems will be used in Section 6 3 Disjointness can be defined by the paragraphs syntax dj inrel 45 46 Z EVES Project TR 99 5493 06a x _dj_ PX e PX disabled rule djDef VA B PXeAdjBSANB OH We have attached a label disabled rule djDef to the defining predicate This lets us give the associated theorem a name that can be used in proof commands allows a usage to be specified determining how the automatic prover commands can use the theorem and allows the theorem to be disabled Here the defining ax
78. rd u password password active active U u We begin by running Z EVES which will eventually display an empty Specification window 10 Z EVES Project TR 99 5493 06a Selecting New Paragraph from the Edit menu brings up the Edit window After clicking the mouse in the edit area we can type User Word File Edit Enabled Disabled NONE User Word ome ee es ET mc Ode e e Subscripts E E E E Cl ee E Tos ayrini EE a a EU J ea AER a a aja meme della After select Done from the File menu in the Edit window the Specification window now shows the new paragraph File Exit Command Window Abort Eager j Syntax Proof Specification gt o User Word RIZR N S Y Y Z EVES Project TR 99 5493 06a 11 The two status bars to the left of the paragraph show question marks showing that it is not known to be correct We can check the paragraph by double clicking on it or by right clicking on it and selecting Check from the pop up menu When the paragraph is checked the status bars are updated File Edit Command Window ebort Eager JEAN Syntax Proof Specification IX Y Y User Word ASS y Y The paragraph is also selected and so is highlighted Both columns contain Y the syntax and type check succeeded and there is nothing interesting to prove The state schema can be added similarly Selecti
79. rectly rendered in the Specification window Selecting Done from the File menu adds the paragraph to the specification Double clicking on the paragraph in the Specification window checks it Appa 200 coger MN Syntax Proof Specificati Y Y N N User Word zmz This time there are errors Right clicking on the paragraph and selecting Show Errors from the pop up menu shows the error messages Z EVES Project TR 99 5493 06a 13 Error RelationArgT ype line 2 Type checker type of local active is not the same as the domain of the relation global_c_ Error RelationArgType line 2 Type checker type of local reg is not the same as the range of the relation global_c_ Error TypesNotSame line 2 Type checker types of local reg and global dom local password are not the same Dismiss Evidently active and reg do not have the correct type for the subset relation and the two sides of the equality have different types On inspection we can see we omitted the P operation in the declaration of active and reg that is we wrote reg active User instead of reg active P User This is readily fixed we can right click on the paragraph and select Edit from the pop up menu When the Edit window appears we can click on the U in User a vertical cursor appears just before it Then selecting P from the palette inserts it so that the declaration is correct Selecting Done
80. roof attempts it is rather awkward to work with disjointness The following two sections show how the theory can be developed to improve the situation 6 3 3 Second attempt elimination We may be able to simplify matters somewhat by eliminating occurrences of function _ dj _ and replacing them by the definition in terms of intersection We can do this by labelling the defining predicate as a rewrite rule This will make the reduction commands replace any predicate X dj Y by XnN Y b Z EVES Project TR 99 5493 06a 63 x _dj_ PX PX rule djDef VA B PXo Adj B amp ANB With this revised definition we can recheck the specification and try the example theorems again For InitManagerIsOK the command prove by reduce completes the proof For AddResourcelsHonest the prove by reduce command results in the goal used P Resource A free P Resource Ar Resource A free N used Nr E free Nr used gt used N free U r which we saw in our earlier proof attempt We can complete the proof using some set theory rule distributeCapOverCupRight transforms the conclusion to user N free U used N r which can be proved automatically by rewriting The complete proof is then proof prove by reduce apply distributeCapOverCupRaght prove The proof has been successful However the proof is still not as simple as we might like an obvious fact like this should be proved immediately The proof
81. rs to subtle inconsistencies in meaning These errors are discussed in Section 3 1 Z EVES can help specifiers avoid many of these errors There is a benefit to a formal specification that goes beyond its precision Formal specifications can be manipulated allowing properties of the specification or the specified system to be explored One simple operation is the expansion and simplification of a schema definition which might help a reader better understand the meaning of a complex specification or might help a designer when it is not possible to structure the implementation in the way the specification is structured A specification is a model of the specified system and can sometimes be used as a sort of prototype It might be possible for example to determine the effect of a certain sequence of operations by calculation Similarly it may be possible to show that a system never gets into an undesirable state by stating and proving appropriate theorems Section 3 2 shows how Z EVES can be used to manipulate specifications in these and other ways 3 1 Checking for Errors Z EVES can help specifiers avoid many different kinds of error However except for syntax and type checking the analyses described in this section are not mandatory Domain checking is strongly recommended and the domain checks are automatically generated but can be omitted if desired The user must decide what kind of analysis is appropriate or cost effective 3 1 1
82. s always ordered efficient searching algorithms are possible e An analyst might wish to verify that the operations of a system preserve some important safety properties The conditions on an invariant are directly expressible in Z and so no special mechanisms are needed in Z EVES to allow their proof Here is a trivial example of an invariant proof Our system has a simple state consisting of a number State n Z initializes the number to zero 28 Z EVES Project TR 99 5493 06a Init State n 0 and provides an operation to increment the number Inc A State n gt n Obviously n gt 0 is an invariant of the system theorem SystemInvariant Init gt n gt 0 A UncAn gt 0 gt wn gt 0 This can be proved with the reduce or prove by reduce commands It is usually convenient to name the invariant e g in the above example to define NonNegative State n gt 0 and to express the invariant theorem as theorem SystemInvariant Init gt NonNegative A Inc A NonNegative gt NonNegative A larger example of an invariant proof has been published 3 The usual Z style includes all the significant invariant properties in the state schema and so invariant proofs are not that common The analyst s job is thus easier the important properties are obviously maintained The implementor who wants to simplify the state schema can use a refinement proof instead of an invaria
83. s zed style for TFX 2 09 Spivey s guide 14 provides details of the markup form However for the z eves package in ATpX2e the beginning of a file must be documentclass article usepackage z eves Other document classes e g report or slides are allowed A IXT X specification can be read by the Import function in the File menu Importing a file adds its paragraphs to the current specification A file can be imported a second time in which case the paragraphs are updated Paragraphs are identified only by their order of occurrence in the IAT X file so this updating only works properly if paragraphs are revised or new paragraphs are appended Some features of TAT X such as fuzz declarations e g Ahinrel R are not recognnized by the importer 18 Z EVES Project TR 99 5493 06a Chapter 3 Analysing Z Specifications The use of Z or any other formal notation in a specification is a great step forward natural language specifications are notorious for their ambiguity Making formal statements about a system can in itself be beneficial as it can lead to a careful consideration of the important aspects of the system and to the development of a consistent terminology However just because a specification is expressed in a formal notation does not mean it is correct complete or even meaningful There are several different kinds of errors that might appear in a specification ranging from trivial spelling erro
84. show the satisfiability of the definition erp LZxN 2 Va Z n Ne exp z 0 1 A exp z n 1 z x exp z n we need to prove Jerp LxN Ze Va Z n Ne exp z 0 1 A exp x n 1 z x exp z n There is no convenient expression to use for exp here the most obvious candidate is defined recursively and Z provides no facility for recursive definitions However the Z EVES Mathematical Toolkit offers a theorem generalPrimitiveRecursion that shows that functions like exp exists theorem generalPrimitiveRecursion Result Parameter Y base Parameter Result step Result x N x Parameter Result e df N x Parameter Result e Vp Parameter e f 0 p base p A Vn Ne f n 1 p step f n p n p Unfortunately and rather typically this theorem gives us a function that takes its arguments the wrong way around However it is possible although rather excruciating to use this theorem to show that exp exists The full proof can be found in the examples directory distributed with Z EVES It is not always possible to show consistency one paragraph at a time sometimes a group of paragraphs need to be considered as a whole This is often the case for a constraint paragraph For example consider the two paragraphs count Z count 0 99 which in a real specification might be separated by several other paragraphs These need to be combined before showing consistency In general it might be necessary to co
85. st forward rules and assumption rules have an indirect effect by adding facts to the context as a goal is traversed The Z EVES Mathematical Toolkit is full of rewrite rules For example it contains the rules theorem rule applyld X Va Xe idX x xz with condition z X pattern id X z and replacement x and theorem rule inRange Va b Zerea bea lt a lt b with condition a Z A b Z pattern z a b and replacement a lt z lt b Consider now working on the predicate 0 lt id 1 5 2 Rule applyld applies to the term id 1 5 2 This term can be replaced by 2 if the subgoal 2 1 5 can be shown Rule inRange applies to this subgoal this has the conditions 1 Z A 5 Z These are simplified to true by arithmetic reasoning so the original subgoal 2 1 5 is replaced by 1 lt 2 lt 5 Arithmetic reasoning replaces this by true So the conditions of applyld are true and so id 1 5 2 is replaced by 2 The whole goal is now 0 lt 2 which simplifies to true Rewrite rules may be disabled when they are declared This is useful in cases where some fact is expressed in the form of an equality or equivalence so it is a syntactically valid rewrite rule but where it might not be a good idea for Z EVES to use the rule automatically during every rewriting step For example the principle of extensionality is declared disabled theorem disabled rule extensionality X YS Vae XereVYyAVy YeyeX It
86. t appear before the theorems whose proofs they are used in Z EVES offers two modes of operation Eager and Lazy In Eager mode the rules of checking are strict a paragraph can only be checked if all preceding paragraphs have been checked As one s goal is to have the entire sequence of paragraphs checked this is reasonable Lazy mode allows paragraphs to be skipped This can be useful in experimentation for example the specification might contain two alternative versions of a paragraph In Lazy mode one of these can be checked and the other left unchecked and the remainder of the specification can be analysed The status bars help a user to keep track of the experiment by showing what has been checked and what has not By default Z EVES is in the Lazy mode When paragraphs have been checked their phrase structure is browsable in the specification window When the mouse is clicked over a part of a checked paragraph the smallest containing phrase i e name expression predicate or paragraph is highlighted Successive clicks will cause larger and larger containing phrases to be highlighted Alternatively the mouse can be moved with the left button depressed in which case the smallest phrase containing both the place where the button was first depressed and the current location of the pointer is highlighted A selected part can be copied to the clipboard by selecting Copy from the Edit menu in
87. ter 4 The Z EVES Prover The Z EVES prover combines automatic strategies and detailed user steps allowing for a collabo rative effort in completing a proof Z EVES can look after mundane details such as side conditions on proof steps and trivial subgoals leaving the user free to focus on the main line of argument of a proof Z EVES offers some powerful automatic commands for proving theorems e g prove or reduce However these commands will only succeed in proving easy theorems and then only when the way has been prepared For example when a name is defined by an abbreviation definition axiomatic box or generic box it may be necessary for some simple theorems to be stated before the automatic steps can succeed In this chapter we will describe the Z EVES proving mechanisms in detail later chapters will offer guidance on how to use these mechanisms effectively There are two main aspects to effective use of the prover first guiding the proof and second developing a theory in a way that supports the prover s capabilities Even with the best use of the automatic capabilities of the system however there will be proofs that are not fully automatic Indeed this is likely to be the rule rather than the exception In these situations the Z EVES user needs to know a proof or at least an outline of a proof Z EVES can then be used to check this proof ensuring that all side conditions are satisfied and perhaps to fill in any missing
88. that apply to predicates that commonly occur as side conditions in a proof A common type of rewrite rule replaces an expression or predicate by something simpler For example the fact VS PX e S S is an obvious candidate for a rewrite rule the replacement expression S is always simpler than the pattern S Similarly the fact X X is suitable as a rule 3 Not all theorems make good rules While it is useful to identify theorems that can be rewrite rules one should be judicious For example the Z EVES mathematical Toolkit contains a number of distribution laws including AU B N C AUB N AUC This could possibly be a rewrite rule but it is not obvious which form of expression is superior Similarly the equality R R is a possible rewrite rule but it is not obvious that one form should be preferred to the other These facts are disabled rewrite rules in the Toolkit so they can be applied if desired but are not normally applied A fact might be a poor rewrite rule because it introduces complexity For example p Xx Y amp da X y Y e p 2 y can be added as a rewrite rule but doing so makes rewriting introduce many quantifiers into a predicate Again it is better to state such facts as disabled rules so they can be applied when and if they are appropriate in a proof 4 Make theorems strong Suppose we have defined the notion of increasing and decreasing sequences We could then state a theor
89. the menu bar 2 2 2 The Proof window The Proof window provides three functions inspection and modification of a proof script interactive construction of a proof and proof browsing A proof script is a sequence of Z EVES prover commands Like the specification these commands are displayed along with their status which indicates whether the command has been executed or not Like paragraphs within a specification individual steps can be inserted deleted moved or modified If a proof script is active its steps can be executed and the proof can be browsed In this case below the proof script is a display labeled Formula showing a goal predicate and the script contains an action point that appears in the script The action point shows what stage in the proof script the formula corresponds to There are four browsing buttons on the right side of the top menu bar e lt lt moves the action point to the start of the proof thus displaying the original goal predicate e lt moves the action point back one step e gt moves the action point forward one step and 6 Z EVES Project TR 99 5493 06a e gt gt moves the action point to the end of the proof The action point can also be moved by selecting it right clicking selecting Move from the pop up menu then clicking on a command or just after the last command The interstion point will be moved to just before the selected place Edit Windo
90. tober 1999 A Smith On recursive free types in Z In Nicholls 8 pages 3 39 J M Spivey The Z Notation A Reference Manual Prentice Hall International Series in Com puter Science 2nd edition 1992 Mike Spivey A Guide to the zed style option December 1990 Available by ftp from host ftp comlab ox ac uk in directory pub Zforum as file zguide ps Z Also accessible from http www comlab ox ac uk archive z html J C P Woodcock and J Davies Using Z Specification Proof and Refinement Prentice Hall International Series in Computer Science 1996 67
91. ts of the Prover a 35 LEL Loge emirato de eee le Gee SSE bh wr eee ed 35 41 2 he current theory es eed SR A i ee ds GRRE SS 36 da Proot style 4 3 64 344 a At eine o ek b hoki ee a BAAS 37 4 2 Automation nse s a beat dow eh ee Be Se oe PALES 39 4 2 1 Traversal and reduction 0 0 ee ee 39 4 2 2 Simplification saa eh fa kok ede a Be Be Ge ele a a ee a DA 40 4 20 32 AREWTHNE nd a ae E ee Oe ta A a 42 4 2 4 Reduction and invocation ooo a 43 dido Prove loops esete daria eet oda wae ee EG aa a4 4 44 5 Proving Theorems 5 1 Explorative Proving 5 2 Planned Proofs 6 Theory Development 6 1 6 2 6 3 Objectives 0 ee ee ee 6 1 1 Logical adequacy 6 1 2 Practical adequacy 6 1 3 Automation Guidelines A Theory Development Example 6 3 1 A resource manager 6 3 2 A first proof attempt 6 3 3 Second attempt elimination 6 3 4 Third attempt developing a theory Z EVES Project TR 99 5493 06a Chapter 1 Introduction This user s guide describes how and why to use Z EVES to develop or analyse a Z specification This is not a tutorial on Z there are already a number of readily available books describing Z and its application e g those by Barden et al 2 Hayes 4 Jackey 6 Potter et al 9 Spivey 13 and Woodcock and Davies 15 We assume the reader has a solid grounding in the Z language and its use instea
92. uce use nonEmptySetHasMember S free prenez instantiate r 1 prove E We are left with the goal used P Resource A free P Resource A free A used dj free An free A used dj free x gt dr Resource e r free A used dj free r Bringing in the appropriate instance of djMonotone completes the proof proof use djMonotone Resource A used A used B free B free x prove a These proof scripts seem reasonable the obvious facts about disjointness were proved automati cally and little of the proof of AllocIsHonest had to do with disjointness Of course this single test drive of the theory of disjointness does not show that it is finished and it is quite likely that a more realistic resource manager would require additional properties Another way to test the theory is with small examples In this case the rules we have defined so far are enough to let rewriting show 1 2 3 dj 4 and 1 2 3 dj 10 20 are true and 1 2 3 dj 2 20 is false So the theory seems to be reasonably well developed There is a danger in developing a theory like this what if the axioms are incorrect It is easy to overlook some small detail in stating such theorems and a missing detail can make a supposed theorem unsound So these theorems should all be proved In fact we already proved most of these theorems in Section 5 1 and the remainder are similar we will therefore n
93. ults in the goal REX Ss Y gt Ve Ree dom X Y R x ran X Y R We next wrote let e R be arbitrary this corresponds to a prenex command available in the Quantifiers menu which results in the goal REX Y NeEeR gt e dom X Y R x ran X Y R Step 4 was captured in lemma thm1 which we will bring in with the command use thmi X Y which must be added as a new command and typed in to the editor This results in the goal REexX YAeeRSecexxY AREX OY ACER gt e dom X Y R x ran X Y R Normally after a use command we apply a prove command to clean up the goal If we try that here the added lemma is eliminated and we are left with the goal we had before the use command So before cleaning up we will move on to step 5 where e X x Y is used This step is to infer Jx X y Y eo e x y from e X x Y This is the gist of theorem InCross2 in the Toolkit We can apply the theorem as it is a rewrite rule by selecting X x Y in the goal predicate right clicking and selecting InCross2 from the Apply to expression submenu This results in the goal REXeYn ecRs 3x X y Yee z y AREX OY NeER gt e dom X Y R x ran X Y R lIt seems strange that even though this fact is so obvious to Z EVES we need to bring it in There is in fact a good reason to add e X x Y once it is explicitly in the formula other commands can be applied to it as seen the the remainder of this proo
94. used for r The Toolkit contains the theorem theorem nonEmptySetHasMember S v da Se true 3There is a slight flaw in the way that the current version of Z EVES checks use commands so in this version it is simply impossible to bring in the needed instance of the axiom 62 Z EVES Project TR 99 5493 06a This theorem lets us bring in the fact 3x free e true prenexing eliminates the quantifier on 2 then r can be instantiated Following this we use the prove command to clean up the goal proof use nonEmptySetHasMember S free prove instantiate r 2 prove a The result of these steps is the new goal used P Resource A free P Resource A x free A used dj free Na free Az used U x dj free x gt dr Resource e r free A used U r dj free r in which the two disjointness hypotheses are contradictory We can eliminate function _ dj _ clean up and see where we are proof use axiom 4 Resource A used U x B free z use axiom 4 Resource A used B free prove a Now the goal is used P Resource A free P Resource A x free A used dj free A 7 free A used U x dj free x A free N used A 7 used Up N free x gt dr Resource e r free A used U r dj free r The hypotheses are still contradictory but further proof steps are required to show it As can be seen from these three p
95. ve commands This might be significantly faster than proofs that expand the definition More significantly however if the proof fails then the resulting goal will be more compact and easier to read if the schemas are not expanded 4 2 3 Rewriting In rewriting Z EVES performs simplification and also applies rewrite rules where possible A rewrite rule in general is a theorem having the form Condition gt Pattern Replacement or Condition gt Pattern lt gt Replacement where Condition is a predicate and Pattern and Z EVES Project TR 99 5493 06a 43 Replacement are both expressions or are both predicates In the rewrite command when a sub formula is considered during traversal a rewrite rule can be applied if its pattern matches the subformula e the subformula is an instance of the pattern In this case the corresponding instance of the condition is considered If the condition is recognized as true then the subformula is replaced by the corresponding instance of the replacement This new subformula is then traversed again so that further simplifications rewritings or reductions are possible Rewrite rules are the most easily used automation mechanisms Unlike assumption rules and forward rules which have an effect only on the context rewrite rules cause explicit changes to the goal predicate Furthermore rewrite rules can be applied with the apply command which has an immediate effect on the goal predicate In contra
96. w lt lt gt gt gt Run Proof Script for djNullRight T apply d Def to predicate A amp j X ft action point Y prove by rewrite Fr EEE Reduction Cases Quantifiers Normal Forms Equality Formula AePX ifAePX afte PX then An X f DX else A HX H E PV The illustrated proof window shows a proof script with two steps both of which have been run The user has selected the back button and moved the action point one step back and the Formula area shows the goal predicate that resulted from the application of the first command Commands can be added to a proof script in several ways e New Command can be selected from the Edit menu This exposes the Edit window which allows the command to be composed The new command is added to the end of the script when Done is selected from the File menu in the Edit window Alternatively Cancel can be selected from the File menu in which case the edit is abandoned e A Paste operation inserts the contents of the clipboard immediately before the insertion point where the blinking cursor is in the script window or at the end if there is no insertion point e Some proof commands are available from a menus on a bar above the goal predicate display These commands are entered at the action point and are immediately executed Unfortunately not all prover commands are available from menus and for
97. with no further simplification Jk Zo1 lt kAk lt 3n2 k The simplify command in the Reduction menu applies the one point rule when possible 2 Z For technical reasons the application of the one point rule often results in the type conditions of the quantification remaining unsimplified A final simplify step completes the proof giving the goal predicate true Here is an example of a more realistic proof in Z EVES using an explorative style as described in Chapter 5 theorem Simple Theorem2 Vk Neid 1 k seqN The prove command in the Reduction menu often completes simple proofs automatically and otherwise usually eliminates the uninteresting parts of a conjecture so we apply it here It does not complete the proof here but results in the predicate keZAk gt 0 gt id 1 k seqN We will appeal to the definition of seq Clicking on the seq in the goal predicate highlights it right clicking exposes a pop up menu Selecting Expand this name directs the prover to use the definition of seq giving the new goal predicate keZAk gt 0 gt id 1 k f N gt N 3n Nedom Z N f 1 n A prove command gives kEZAKk gt 0 gt In Nek nVk lt lAn lt l Z EVES was not able to find the right instantiation for n We can specify the correct instance in a proof step There is no convenient gesture in the interface for instantiating so it is necessary to select New Command from the E
98. would be absurd to replace every equality in a formula by a consideration of elements A disabled rule may be used in the apply command or can be enabled for the duration of a reduction command by the with enabled command modifier For example in proving 1 5 N 3 7 3 5 the reduction commands make no progress The command apply extensionality gives a consideration of elements of these two sets the command prove then lets Z EVES finish the proof During a proof the disabled rewrite rules that are applicable to an expression or predicate appearing in the goal predicate can be determined by selecting the expression or formula right clicking and examining the Apply to expresion or Apply to predicate submenu of the pop up menu Selecting one of the names in the list causes it to be applied to the selected expression or predicate If the rule is conditional the result has the form if Condition then Replacement else Original so further proof steps e g rewrite or prove are usually needed 4 2 4 Reduction and invocation In reducing Z EVES performs simplification and rewriting and if a subformula is a schema reference or reference to a name defined as an abbreviation the subformula will be replaced by the definition 44 Z EVES Project TR 99 5493 06a of the schema or abbreviation and the result will again be reduced As well conditional rewrite rules apply if their conditions can be shown to be true by reducing The reduce com

The Z/EVES 2.0 User's Guide - University of Waikato: Department of

Contents

Download Pdf Manuals

Related Search

Related Contents