# CSE503: Software Engineering Lecture 16  (February 10, 1999)

## David Notkin

Ø      Relationship to theorem proving?

Ø      Iterative nature of increasing confidence in a specification

Ø      Others?

v     Z-style specifications

Ø      Brief review of static and dynamic schema

Ø      Brief review of the notation

§        Atomic types

·        Some built-in (like integers)

·        New ones can be declared (like NAME in the birthday book)

§        Three kinds of composite types

·        Set types: a set containing elements of a given type

¨      {1,2,4,8,16}

¨      {p : PERSON | age(p) >16 }

·        Cartesian product types:  tuples containing elements of (potentially) different types

·        Schema types: essentially bindings, but beyond our scope

§        Relations and functions

·        These are represented in Z as sets of tuples, where every tuple in the set represents an element in the specified relation or function

·        There is also special syntactic sugar

¨      X « Y represents the set of binary relations between the sets X and Y

¨      X ®  Y represents the set of total functions between the sets X and Y (and adding a vertical bar in the middle of the arrow represents partial functions)

·        These are mathematical entities, not algorithms or rules for computation, so one can (like in math) compare for equality across them, etc.

·        All of the above entities have the same type: P (X ´ Y) (where P represents the powerset operator)

§        There are a number of other standard parts of the notation: universal and existential quantifiers, basic logic operators, etc.

Ø      Introduce a bit more of the birthday book example

§        Note that the schema describe what happens when the preconditions are met (such as, adding a new birthday only when the name isn't previously known)

§        How should error cases be handled?

·        One choice is to expand the definitions of the schema

¨      This can get unwieldy quickly

·        Another choice is to define the normal and off-normal cases separately and to combine them using the schema calculus

¨      Essentially, the schema calculus allows you to apply logical operators to Z schema

§        As I have mentioned before, this is great at the specification level, but not straightforward at the implementation level

·        What precisely does it mean to conjoin two implementations?

¨      Is there an AOP (aspect oriented programming) characterization of this?

Ø      Final note on Z per se; one of the most noted uses is at IBM, where it was used to helped a major reengineering of the CICS system

§        http://www.comlab.ox.ac.uk/oucl/qata92.html

v     Then tie Z-style specifications to model checking

Ø      Model checking only applies to finite systems since it is, at its heart, enumerative

Ø      But many Z-style specifications are infinite systems, at least with respect to the issue of data

§        That is, Z integers are mathematical integers, for instance

Ø      One approach to handling infinite state systems using techniques for finite state systems: abstraction.  One builds a finite abstraction of an infinite state system that captures key aspects of the system, and then analyzes or checks that abstraction

·        In all such cases, one is concerned with some questions like:

¨      If a property is proven to be true in the abstraction, do we know if it holds in the original system?

¨      If a property is proven to be false in the abstraction, do we know if it is false in the original system?

Ø      Jackson and Damon took a somewhat different approach (Nitpick)

§        They use enumeration, as in model checking, but they explicitly truncate the state space that they check

·        For example, for integers, they might try all combinations of values up through 5 or 10

·        They then report on any counterexamples they find within that truncated state space

¨      Ex: If there are four phones in use simultaneously, then there is a situation in which one phone is connected to no conversations; this might be a counterexample for a desired property (that any phone in use is involved in a conversation)

§        They have several implementations of this, and several examples

·        One implementation uses explicit model checking, with (smart but) actual enumeration of all the states

·        Another implementation uses symbolic model checking

·        Usually, the symbolic version is faster, but in some cases it doesn't work at all (and there is no obvious way to determine when and where it works and doesn't)