Sets and constants
Constants
Concrete constants
Properties and not values
Sets
Enumerated sets
Deferred Sets
Explicitly list the elements of the set
Valued by intervals of integers
Directly implementable
Don't require further refinement
Abstract constants
Can't be defined in implementation
The conditions they respect are declared in the PROPERTIES clause
Visibility
PROPERTIES is able to read sets and constants
INITIALISATION can see sets, constants and variables
INVARIANT can see sets, constants and variables
OPERATIONS can see sets, constants and variables
Machine consistency
PROPERTIES feasibility
Prove that there exist a state and a evaluation fir the constants such that the properties are true
There are 2 good ways to ensure the sets and constants' properties
Using the ASSERTIONS clause in a separated machine
Implementing the machine that contain the PROPERTIES clause before moving on
INVARIANT consistency
Proving that there exists an evaluation for the state variables such that the invariant holds
INITIALISATION consistency
Prove that the properties imply that the initialisation establishes the invariant
OPERATIONS consistency
Once the invariant and the precondition hold, then the cammand has to establish the invariant
Now we have that the properties are also true and should be used as the proposition on the LHS
#St, k. B
B => #v. I
B => [T] I
B & I & P => [S] I
Relations
Operations
Cartesian products
A relation is a subset of the cartesian product of two sets
Domain
Range
Domain restriction
Domain anti-restriction
Range restriction
Relational image
Relational inverse
Relational composition
Relational overriding
Range anti-restriction
dom(R) = {x | x:S & #y. (y:T & x|->y:R)}
ran(R) = {y | y:T & #x. (x:S & x|->y:R)}
U<|R = {x|->y | x|->y:R & x:U}
U<<|R = {x|->y | x|->y:R & x/:U}
R|>U = {x|->y | x|->y:R & y:U}
R|>>U = {x|->y | x|->y:R & y/:U}
R[U] = {y | x|->y:R & x:U}
R~ = {y|->x | x|->y:R}
R0; R1 = {x|->z | x:S & z:U & #y. (y:T & x|->y:R0 & y|->z:R1)}
R0<+R1 = (dom(R1)<<|R0) \/ R1