Z Logic and its Consequences

Z Logic and its Consequences
of 33
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
  Computing and Informatics, Vol. 00, 0000, 0–32, V 2003-Jun-16 Z LOGIC AND ITS CONSEQUENCES Martin C. Henson Department of Computer Science, University of Essex, U.K  Steve Reeves Department of Computer Science, University of Waikato, N.Z. Jonathan P. Bowen Centre for Applied Formal Methods, London South Bank University, U.K. Abstract.  This paper provides an introduction to the specification language Z froma logical perspective. The possibility of presenting Z in this way is a consequence of a number of joint publications on Z logic that Henson and Reeves have co-writtensince 1997. We provide an informal as well as formal introduction to Z logic andshow how it may be used, and extended, to investigate issues such as equationallogic, the logic of preconditions, the issue of monotonicity and both operation anddata refinement.For Peter Wexler –  in memoriam  1 INTRODUCTION This paper describes an approach to Z  logic   – it is relatively unconcerned withZ  semantics  , except insofar as the existence of a non-trivial model is useful forestablishing the consistency of the logic. The paper neither attempts to replicate,nor to extend, the excellent work on Z standardisation which has led to ISO standard  Z Logic and its Consequences   113568. 1 It is, rather, complementary, seeking to explore and express the logicalpreliminaries of Z 2 and aiming to describe those uncontroversial properties of themajor elements of the language, in particular, the language of   schemas   and its calculus  .The approach to Z logic taken here is mainly based on three papers [17, 18, 19];these remain the comprehensive technical resource for two separate though relatedapproaches (we make some reference to the distinction in section 3.5). Our objectivein this paper is to provide a more accessible overview of that work and to highlightsome more advanced related work beyond specification, in particular in the theoryof refinement, that becomes possible by virtue of the Z logic that we describe.The paper is structured in three parts. The first is the least formal and mostaccessible: it explores initial considerations concerning the formalisation of vernac-ular 3 Z with particular reference to the novel features (those that take Z beyond, atleast in expressivity, higher-order logic) concerning  schema types   and  bindings  . Thesecond part of the paper is a more formally presented account of Z logic (the logic Z  C ) and how that may be extended by means of a series of conservative extensionsto more comprehensive logical systems with wider coverage. We are by no meansencyclopædic and the earlier papers referred to above contain more detail and amore formal account. The final part of the paper contains the most advanced ma-terial: it looks beyond Z as a specification language and  Z  C  as a logic for reasoningabout specification. It demonstrates the further utility of such a logic by showinghow various theories of equality, operation and data refinement can be integratedwith, and issues such as monotonicity explored within, the base logic in a smoothand systematic manner: something made possible with a logic in place. This surveyrelies on the reader’s previous general knowledge of the topics it briefly surveys.The paper ends with some concluding remarks, our acknowledgements and relevantreferences to the literature. 2 INITIAL CONSIDERATIONS We take it as self-evident that any formal specification should permit precise con-sequences to be drawn: the emphasis in the term  formal method   should fall on thesecond word and not the first. A language, even one with a semantics, is impover-ished if there is no logic: it would provide no means for drawing those consequencesin a methodical, reproducible and agreed fashion. In this first part of the paper we 1 The Z Standard does not provide a logic. The strategic decision to exclude a logicwas reported in [22]. An inconsistency [16] was discovered in the (unfinished) draft logicsubmitted as part of the ISO Committee Draft 1.2 of the Z Standard in 1995. 2 Although beginning from its logical first principles, this paper does not begin Z itself from first principles. The reader is assumed to be familiar with Z notation and conceptsas described in one of the better textbooks, for example, [33]. 3 By  vernacular   Z we refer to Z as it has been used in practice and as it is reported ininformal and semi-formal accounts in the literature.  2  M. C. Henson, S. Reeves, J. P. Bowen  re-introduce the key features of specification in Z from a logical perspective. Ourobjective is to motivate and introduce the basic principles of the logic  Z  C  and toexplain why this core logic is a satisfactory basis for establishing logical apparatusfor a range of Z concepts. 2.1 Z schemas and bindings At the heart of Z is the  schema  . Schemas are usually used in two ways: for describingthe  state space   of a system and for describing  operations   which the system mayperform. Example 1.  Informal state space: a jug of capacity 250ml of water having a currentvolume and a current temperature. As a schema: Jug volume   :  N temp  :  N volume   ≤  250 temp  ≤  100Written in linear form this would be: Jug     = [ volume   :  N ;  temp  :  N  |  volume   ≤  250  ∧  temp  ≤  100]This schema has the name  Jug   and introduces two  observations  ,  volume   and  temp ,which have some natural number value ( i.e.  drawn from the set  N ) in each systemstate. 4 The states which comprise a schema are called  bindings  , each binding be-longing to a schema is a legitimate state of the system. In this example the bindingsassociate values (of the correct type) to the observations named  volume   and  temp .We use the word “observation” and  never   call them “variables”. If one pursuesthe “schemas as sets of bindings” interpretation (which has been quite standard)then these are constants, not variables. Most informal accounts run into immediatedifficulty in this area 5 .We will write bindings like this: 6 |  volume   ⇛  n  , temp  ⇛  m   | 4 Note that the schema describes a  state space  , that is, a set of legitimate system states.This is worth stressing because some informal accounts give a mixed message, sometimessuggesting that a schema describes a  particular   state. 5 See for example [33]. In chapter 11, page 149, they are “variables”; by page 154 theyare “components” (constants). 6 ISO Z uses == rather than  ⇛ , a notation which dates back to [28] and [29].  Z Logic and its Consequences   3where, in this case,  n   ∈  N  etc.  Naturally, it  should   follow that, for example: |  volume   ⇛  100 , temp  ⇛  20  | ∈  Jug  and also: |  volume   ⇛  100 , temp  ⇛  200  | ∈  Jug  It is possible to extract the values associated with observations from bindings. Thisis called  binding selection  . For example, we should be able to show: |  volume   ⇛  100 , temp  ⇛  20  | . volume   = 100In order to capture these ideas we begin by introducing the idea of a  schema type  : [ ···  z T  i  i   ··· ] This is an unordered sequence of typed (indicated by superscripts) observations (the z i  ). Then  schemas   are either  schema sets  : [ ···  z i   :  C  P T  i  i   ··· ] or they are  atomic schemas  : [ S   | P   ] where the  C  i   are sets,  S   is a schema and  P   is a predicate.Of particular note are the  carrier sets   of the various types. These are formedby closing: N  = df   { z  N |  true  } under the cartesian product, power type and schema type operations. 7 No ambiguity results from the overloading of the symbol  N  here: types appearonly as superscripts – all other uses denote the carrier set.We have remarked that schemas are  sets of bindings  . So the logic of schemascan be obtained from the logic of sets and bindings. In  Z  C , for sets, we have: P  [ z  / t  ] t   ∈ { z   |  P  }  ( {} + )  t   ∈ { z   |  P  } P  [ z  / t  ] ( {} − )Note that  Z  C  is strongly typed, so these (typed) set comprehensions present notechnical difficulties. See section 3 for further details.For bindings,  Z  C  has: | ··· z i  ⇛ t  i   ··· | . z i   =  t  i  ( ⇛ =   ) | ··· z i  ⇛ t  . z i   ··· |  =  t  [ ··· z Tii  ··· ] ( ⇛ =   )The first of these establishes what information may be extracted from bindings; thesecond confirms that these values are  all   that the binding contains. 7 In fact  N  is only one possible base type. See section 3 for further details.  4  M. C. Henson, S. Reeves, J. P. Bowen  The logical rules for schemas flow from the following  Z  C  definitions: [ ···  z i   :  C  i   ··· ]  = df   { x   | ··· ∧  x  . z i   ∈  C  i   ∧ ···} and: [ S   | P   ]  = df   { z   ∈  S   | z  . P  } The  binding selection   operator, introduced in the object logic for selection from bind-ings (that is,  Z  C  terms such as  z  . x ) is generalised into a meta-language substitutionover terms (that is, meta-terms such as  z  .t) and over propositions (meta-terms suchas  z  .P) 8 . This is essentially a straightforward structural recursive generalisation of binding selection, and appears in more detail in section 3 below.The rules for  schema sets   are then derivable in  Z  C : ···  t  i   ∈  C  i   ···| ··· z i  ⇛ t  i   ··· | ∈  [ ··· z i   :  C  i   ··· ] ([] + )  t   ∈  [ ··· z i   :  C  i   ··· ] t  . z i   ∈  C  i  ([] − )and, for  atomic schemas  : t   ∈  S t  . P t   ∈  [ S   |  P  ] ( S  + )  t   ∈  [ S   |  P  ] t   ∈  S   ( S  −   )  t   ∈  [ S   |  P  ] t  . P   ( S  −   )Then for example, writing  b  for  |  volume   ⇛  100 , temp  ⇛  20  | , we have:....100  ∈  N  ∧  20  ∈  N b  ∈  [ volume   :  N , temp  :  N ] ([] + )....100  ≤  250  ∧  20  ≤  100 b  ∈  Jug   ( S  + )as expected, with the trivial steps omitted.The elimination rules allow us to determine properties of specifications. Forexample, taking the product of the temperature and the volume as a rudimentarymeasure of the thermal energy of the water, we can show that this is never biggerthan 25000: b  ∈  Jug   1 , ( S  −   ) b . volume   ≤  250  ∧  b . temp  ≤  100 b . volume   ∗ b . temp  ≤  25000 ∀ b  ∈  Jug   •  b . volume   ∗ b . temp  ≤  25000 1 2.2 Schema algebra and filtered bindings Having now considered simple schemas, we will move on immediately to consider anoperation from the schema calculus:  schema conjunction  . 8 This is modelled to some extent on the more complex  object language   substitution  frogspawn   operator to be found in the faulty logic presented in [26]. A thorough analysisof frogspawn terms is presented in [19].
Similar documents
View more...
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks

We need your sign to support Project to invent "SMART AND CONTROLLABLE REFLECTIVE BALLOONS" to cover the Sun and Save Our Earth.

More details...

Sign Now!

We are very appreciated for your Prompt Action!