Scribd
Upload
59 views

Assertional Reasoning: COMP2111 Lecture 4a Session 1, 2013

The document describes transition diagrams, which can represent sequential programs. A transition diagram consists of locations, transitions between locations, an entry location, and an exit location. Transitions are labeled with conditions and state updates. Computations in a transition diagram may terminate normally, fail, or diverge. The semantics of a transition diagram maps initial states to possible outcomes. Floyd's method can be used to prove partial correctness assertions {φ}P{ψ} by defining an inductive assertion network that relates precondition φ to the entry location and postcondition ψ to the exit location.

Uploaded by

Jordieee
Copyright
© Attribution Non-Commercial (BY-NC)
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
59 views

Assertional Reasoning: COMP2111 Lecture 4a Session 1, 2013

The document describes transition diagrams, which can represent sequential programs. A transition diagram consists of locations, transitions between locations, an entry location, and an exit location. Transitions are labeled with conditions and state updates. Computations in a transition diagram may terminate normally, fail, or diverge. The semantics of a transition diagram maps initial states to possible outcomes. Floyd's method can be used to prove partial correctness assertions {φ}P{ψ} by defining an inductive assertion network that relates precondition φ to the entry location and postcondition ψ to the exit location.

Uploaded by

Jordieee
Copyright
© Attribution Non-Commercial (BY-NC)
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 13

Transition Diagrams

COMP2111 Lecture 4a Session 1, 2013

Assertional Reasoning
Kai Engelhardt

Revision: 1.2

Transition Diagrams

Transition Diagrams

Denition Let be a state space. A transition diagram is a quadruple P = (L, T , s , t ), where: L is a nite set of locations T is a nite set of triples ( , c f , ) called transitions, with , L, c : B, and f : s L is the entry location t L is the exit location

Transition Diagrams

Transition diagrams can be thought of as a very simple programming language with conditional branching, where the conditions on the branches need not be disjoint. Or we could use them as an intermediate language to represent sequental programs. NB Note the dierence between these transition diagrams and those introduced in se2011, which have || = 1.

Transition Diagrams

Example (Transition Diagram) A statement such as while (x > y) x--; can be understood as the transition diagram

true x --

x y l1 x >y l2 t

Transition Diagrams

A Familiar Example

initialisation of low,high while condition on low,high assignment to mid in terms of something like (low+high)/2 if comparison involving A,a and mid then assignment to low in terms of mid else assignment to high in terms of mid

Transition Diagrams

A Familiar Example

s
1 2 3 4 5

initialisation of low,high while condition on low,high assignment to mid in terms of something like (low+high)/2 if comparison involving A,a and mid then assignment to low in terms of mid else assignment to high in terms of mid

Transition Diagrams

Execution Model
Denition A computation (L ) starting in an initial state 0 is a (nite or innite) sequence of congurations : 0 , 0 1 , 1 . . . such that 0 = s , and: For each computation step i , i i +1 , i +1 there exist c and f such that
1 2 3

( i , c f , i +1 ) T , c (i ), and i +1 = f (i ).

The sequence cannot be extended, i.e., if the sequence is nite, its last conguration has no possible successors.

Transition Diagrams

Classifying Computations
Each computation belongs to precisely one of three classes:
1

The sequence is nite, and its last conguration is of the form t , for some . Such a sequence is called a terminating sequence. The sequence is nite, but its last conguration is not of the previous form. This must therefore be a deadlock conguration, that is, there doesnt exist a transition ( , c f , ) T departing from the last location = 1 = t in such that c ( 1 ). Such a sequence is called a failing sequence. The sequence is innite. Such a sequence is called divergent.

Transition Diagrams

Semantics
Denote by [[P ]] the set of all computations of P starting with the initial state . We dene the meaning of the sequential transition diagram P as a function: M(P ) = { val ( ) : [[P ]] } where val ( ) is
1 2 3

if terminates and its nal conguration is t , , or fail if fails, or if diverges.

Thus the meaning of a transition diagram P is a function which for a given initial state gives the set of all possible outcomes, including the possibility of divergent and of failing computations ( M(P ) or fail M(P ) ).
9

Transition Diagrams

Partial Correctness

Let be a state space, let P = (L, T , s , t ) be a transition diagram, and let , : B. We say that {} P { } i ( ) M(P ) ( ), for all , . Observe that this captures partial correctness because we simply ignore all potential failures and divergences of P .

10

Transition Diagrams

Assertion Networks
Question How can we prove {} P { }? Denitions An assertion network for transition diagram (L, T , s , t ) is a function Q associating a predicate Q with each location L. The (local) verication condition for transition = ( , c f , ) is

Q c Q f .

The symbol (circ in Event-B) denotes function composition. For functions f : A B and g : B C we dene g f : A C by (g f )(a) = g (f (a)), for all a A.
11

Transition Diagrams

Floyds Inductive Assertion Method

Denition An assertion network is called inductive if all verication conditions are valid, that is, true in every state. Theorem (Floyd) If the assertion network Q is inductive and the two implications Qs and Qt are valid, then this proves {} P { }. Observe that the number of verication conditions arising from a proof of {} (L, T , s , t ) { } using Floyds method is 2 + |T |.

12

Transition Diagrams

Proof
It suces to show that the nal states of all terminating computations starting in -states are -states. Let = 0 , 0 1 , 1 2 , 2 . . . k , k be a terminating computation such that (0 ). By induction we show that Q i (i ) for all i {0, . . . , k }. Recall that 0 = s . The rst implication establishes the base case Q 0 (0 ). For the inductive case, assume Q i (i ) for some i < k . Let c and f be such that ( i , c f , i +1 ) T , c (i ), and i +1 = f (i ). By validity of the local verication condition Q i c Q i +1 f for transition ( i , c f , i +1 ) it follows that (Q i +1 f )(i ). By denition of and since f (i ) = i +1 , this implies Q i +1 (i +1 ). Finally, the second implication ensures (k ) when taking k = t into account.

13

You might also like