Schema Operators: Schema Operators
Introduction: Introduction The application of the schema language revolves around the concept of an abstract data type A collection of variables A list of operations that may change their values We may use a schema to express the relationship between the state before and the state after an operation
Introduction: Introduction How the information contained in schemas may be combined in a variety of different ways We introduce a language of logical schema operators: Conjunction Disjunction Negation Quantification Composition
Conjunction : Conjunction We may combine the information contained in two schemas in a variety of ways The simplest of these is conjunction Suppose that S and T are the schemas introduced by
Conjunction: Conjunction We write S ˄T to denote the conjunction of these two schemas A new schema formed by merging the declaration parts of S and T and conjoining their predicate parts
Conjunction: Conjunction The result of a schema conjunction is a schema that introduces both sets of variables and imposes both constraints Schema conjunction allows us to specify different aspects of a specification separately, and then combine them to form a complete description
PowerPoint Presentation: We may also conjoin two schema by including one in declaration part of the other
Decoration : Decoration State invariant for the system: a constraint that must always be satisfied Each object of schema type State represents a valid state: a binding of a and b in which predicate P is satisfied .
Decoration : Decoration To describe an operation upon the state, we use two copies of State One representing the state before the operation Other representing the state afterwards To distinguish between the two, we decorate the components of the second schema i.e. Adding a single prime to each name
Decoration : Decoration There are three standard decorations used in describing operations on abstract data types ´ for labeling the final state of an operation ? f or labeling its inputs ! for labeling its outputs
Decoration : Decoration There is a convention for including two copies of the same schema, one of them decorated with a prime If Schema describes the state of a system, then Δ Schema is a schema including both Schema and Schema´
PowerPoint Presentation: The inclusion of a schema name in a declaration introduces a combination of components An important advantage of the schema notation is that it allows us to refer to this combination as a single entity
Bindings: Bindings
PowerPoint Presentation: The declaration s : SchemaOne introduces an object s of schema type SchemaOne The schema type SchemaOne is a set of all bindings in which a and c are bound to an integer and set of integers, respectively We list the component names and the values to which they are bound. This requires a new piece of notation :
PowerPoint Presentation: Θ Schema , is a binding in which each component of Schema is associated with the value of the variable with the same name If the state of a system is described by schema State , the binding Θ State corresponds to the before state We can describe properties of this binding By equating it to another object of the same schema type The decorated binding ( Θ state)´ associates the components of State with the values of decorated variables Two bindings are equal if they bind their component names to equivalent values
Ξ Notation : Ξ Notation Equating decorated and undecorated bindings of State is thus a way of insisting that the before state is equal to the after state Ξ Schema to denote the schema that includes Schema and Schema´ and equates their bindings
PowerPoint Presentation: The declaration Ξ BirthdayBook indicates that this is an operation in which the state does not change : T he values known´ and birthday´ of the observations after the operation are equal to their values known and birthday beforehand Known´ = known Birthday´ = birthday
Initialization : Initialization The initial state of the system may be described by decorated copy of the state schema, representing state after initialization
Disjunction : Disjunction Schema disjunction allows us to describe alternatives in the behavior of a system We may describe a variety of ways in which a system may evolve, and then combine them to produce a complete description Is S and T schemas introduced by
PowerPoint Presentation: If the same variable is declared in both schemas, as with b above, then the types must match
Negation: Negation If S is a schema , then its negation S may be obtained by negating the predicate part For example, if A and B are types and S is introduced by then S
Quantification: Quantification If Q is a quantifier and dec is a declaration, then the quantified schema Obtained from Schema by removing those components that are also declared in dec and quantifying them with Q in the predicate part
Quantification: Quantification The schema S must have as components all the variables introduced by dec , and they must have the same types The signature of the result contains all the components of S except those introduced by dec They have the same types as in S
Hiding : Hiding The hiding operator \ provide ways of removing components from schemas If S is a schema, and x 1 ,… x n are components of S then Its components are the components of S , except for x 1 ,…, x n , and they have the same types as in S The property of this schema is true under exactly those bindings that are restrictions of bindings that satisfy the property of S
Hiding : Hiding Provided there is no clash of variables, the schema can be written using an existential quantifier : if Gimel is the schema, then Gimel \ ( z) is the schema
Composition : Composition If Op1 and Op2 are schemas describing two operations, then Op1 ⨟ Op2 is a schema which describes their sequential composition The components of Op1 ⨟ Op2 are the merged components of Op1 and Op2, with the matching state variables hidden . In Op1, the components of State´ represent the state of the system immediately after the operation. In the composition, this is also the state of the system immediately before Op2. We introduce a new schema to represent this intermediate state: State´´
Composition: Composition This condition says that any state in which Op1 may finish satisfies the pre-condition of Op2
Composition: Composition Inc ⨟ Add