Formal Specification - Revision history

Suhridk: /* Initial State */

2012-02-06T18:34:53Z

Initial State

2012-02-06T18:34:23Z

Schema Combination

2012-02-05T18:10:33Z

Schema Combination

2012-02-05T15:05:23Z

2012-02-05T13:33:34Z

2012-02-05T13:32:18Z

Operations

2012-02-05T12:50:32Z

Operations

2012-02-05T12:48:49Z

Operations

2012-02-05T12:33:06Z

Operations

2012-02-05T12:27:04Z

Structure of a Z specification

@@ Line 106: / Line 106: @@
 * S3 ≙ S1 ∧ S2
-= Initial State =
+== Initial State ==
 * Initial state is a special after state without a corresponding before state.
 * The state is suffixed with a ' mark in the schema declaration.
 * All state variables are decorated with a ' mark.

@@ Line 100: / Line 100: @@
 * Used for operations which dont change the state.
-= Schema Combination =
+== Schema Combination ==
 * Two schemas S and T can be combined using and, or, implies, equivalence operators.

← Older revision		Revision as of 18:10, 5 February 2012
Line 105:		Line 105:
	* This defines a schema which merges declarations and gives a predicate which is combined using the schema combination operator specified above.		* This defines a schema which merges declarations and gives a predicate which is combined using the schema combination operator specified above.
	* S3 ≙ S1 ∧ S2		* S3 ≙ S1 ∧ S2
		+
		+	= Initial State =
		+
		+	* Initial state is a special after state without a corresponding before state.
		+	* The state is suffixed with a ' mark in the schema declaration.
		+	* All state variables are decorated with a ' mark.

← Older revision		Revision as of 15:05, 5 February 2012
Line 99:		Line 99:
	* Inclduing 𝛯S in an operation schema, where S is a state makes visible before and after version of declarations and predicates together with the assertion that these variables are not changed by the operation.		* Inclduing 𝛯S in an operation schema, where S is a state makes visible before and after version of declarations and predicates together with the assertion that these variables are not changed by the operation.
	* Used for operations which dont change the state.		* Used for operations which dont change the state.
		+
		+	= Schema Combination =
		+
		+	* Two schemas S and T can be combined using and, or, implies, equivalence operators.
		+	* This defines a schema which merges declarations and gives a predicate which is combined using the schema combination operator specified above.
		+	* S3 ≙ S1 ∧ S2

← Older revision		Revision as of 13:33, 5 February 2012
Line 98:		Line 98:

	* Inclduing 𝛯S in an operation schema, where S is a state makes visible before and after version of declarations and predicates together with the assertion that these variables are not changed by the operation.		* Inclduing 𝛯S in an operation schema, where S is a state makes visible before and after version of declarations and predicates together with the assertion that these variables are not changed by the operation.
		+	* Used for operations which dont change the state.

@@ Line 89: / Line 89: @@
 * Postconditions: Predicates which relate the before state and inputs to the after state and outputs.
 * All declarations and predicates are local to the schema and not available in other schema, so the operation must use the delta notation to indicate which schema it is modifying.
 * The delta will bring into scope the before and after versions of the state variables and invariant predicates.
 * Otherwise each before and after variable state as well before and after versions of predicates need to be explicitly specified.

← Older revision		Revision as of 12:50, 5 February 2012
Line 89:		Line 89:
	* Postconditions: Predicates which relate the before state and inputs to the after state and outputs.		* Postconditions: Predicates which relate the before state and inputs to the after state and outputs.
	* All declarations and predicates are local to the schema and not available in other schema, so the operation must use the delta notation to indicate which schema it is modifying.		* All declarations and predicates are local to the schema and not available in other schema, so the operation must use the delta notation to indicate which schema it is modifying.
		+	* The delta will bring into scope the before and after versions of the state variables and invariant predicates.
		+	* Otherwise each before and after variable state as well before and after versions of predicates need to be explicitly specified.

← Older revision		Revision as of 12:48, 5 February 2012
Line 88:		Line 88:
	* Preconditions: Predicates which state what must be true about the before state of the system and the inputs in order for the operations to take place.		* Preconditions: Predicates which state what must be true about the before state of the system and the inputs in order for the operations to take place.
	* Postconditions: Predicates which relate the before state and inputs to the after state and outputs.		* Postconditions: Predicates which relate the before state and inputs to the after state and outputs.
		+	* All declarations and predicates are local to the schema and not available in other schema, so the operation must use the delta notation to indicate which schema it is modifying.

← Older revision		Revision as of 12:33, 5 February 2012
Line 86:		Line 86:
	* Before variables are undecorated.		* Before variables are undecorated.
	* After variables are terminated with a '.		* After variables are terminated with a '.
		+	* Preconditions: Predicates which state what must be true about the before state of the system and the inputs in order for the operations to take place.
		+	* Postconditions: Predicates which relate the before state and inputs to the after state and outputs.

← Older revision		Revision as of 12:27, 5 February 2012
Line 77:		Line 77:
	* Top half contains declarations - state variables and bottom half contains the state invariants.		* Top half contains declarations - state variables and bottom half contains the state invariants.
	* All predicates '''are implicitly and-ed''' together.		* All predicates '''are implicitly and-ed''' together.
		+	* The state schema '''defines the set of valid states''' which the system may assume.
		+
		+	== Operations ==
		+
		+	* The system may move from one valid state to another by operations which change the values of one or more of the state variables.
		+	* Input identifiers terminated with ? and Output identifiers terminated by !.
		+	* State variables need to be referred to the before and after state when an operation takes place.
		+	* Before variables are undecorated.
		+	* After variables are terminated with a '.