Transcript Part 0

Lecture 2:
Reasoning with Distributed Programs
Anish Arora
CSE 6333
Required Reading
•
•
Chapter 2, 1, 3, 4 in Paul Sivilotti's book
www.cse.ohio-state.edu/~anish/763/763HandoutPropositional Logic.pdf
Syntax of programs
•
A program is a set of variables and a finite set of actions
 Each variable has a predefined nonempty domain
 Each action has the form:
<guard>

<statement>
 A guard is a boolean expression over program variables
 A statement updates zero or more program variables
and always terminates upon execution
BNF for our programming language
•
stmt

skip
| assignment_stmt
| parallel_assignment_stmt
| if_stmt
| terminating_do_stmt
| stmt ; stmt
•
action
•
program 

guard  stmt
action (▯ action)*
Semantics for our programming language
Intuition for program execution :
At every step, pick an enabled action.
Execute that action.
Repeat until no action is enabled.
(Note that some action(s) may be unfairly picked at every
step, and other actions may be unfairly omitted even if
they are enabled.)
Semantics of programs
Let p be a program
•
•
•
•
A state of p is defined by a value for each variable of p,
chosen from the domain of the variable
A state predicate of p is a boolean expression over the
variables of p
An action of p is enabled at a state iff the guard of the action
holds at that state
A computation of p is a maximal sequence of steps; in every
step, some action in p that is enabled in the current state is
executed
 Maximality of the sequence means that if the sequence is
finite then no action in p is enabled in the final state
Examples of programs
Example 0 :
• Given : X,Y : integer constants
o,x,y : integer variables
•
Design :
(X >0  Y >0  x=X  y=Y) leads-to o=gcd(X,Y)
program EUCLID
▯
▯
x>y

x  x - y
y>x

y  y - x

o  x
x=y
o x

Examples of programs
Example 1 :
•
•
Given :
Design :
x:
array 0..N-1 of integer
k, j, m :
integer
(k = 0  j = 0  m = 0) leads-to (x is in nondec
order of INIT_x)
program BBSORT
▯
k<N
 (if x.k < x.m then m  k) ; k = k + 1
k=N
 x.j, x.m, j, k, m  x.m, x.j, j+1, j+1, j+1

j<N
Examples of programs
Example 2 :
•
•
Given :
x : array 0..N-1 of integer
Design :
true leads-to (x is in non-decec order of INIT_x)
program HYSORT
parameter
▯
(j,k) :
j<k
j, k : 0 …. N-1

x.j > x.k

x.j, x.k  x.k, x.j
Specifications
•
A specification consists of a safety specification and
a liveness specification
 A safety specification identifies a set of "bad" finite
computation prefixes that should not appear in any
program computation
 Dually, a liveness specification identifies a set of "good"
computation suffixes such that every computation has a
suffix that is in this set
•
Thus, a specification identifies a set of computations, none
of which contain a bad prefix and all of which contain a
good suffix
Specifications (contd.)
•
For convenience, we will assume that a specification are
suffix closed
 suffix closed means that every suffix of a computation in
a specification is also in the specification
•
We say that a program computation satisfies a specification
if the former is in the set of computations identified by the
latter
Program Correctness
•
•
•
•
•
Program p is correct with respect to its specification
iff every computation of p satisfies the specification
In other words, every computation in p has no bad prefix,
as identified by the safety specification, and has
some good suffix, as identified by the liveness specification
Safety captures the intuition that nothing bad ever happens
Liveness captures the intuition that something good happens
eventually
Note that since the specification is suffix closed, if a program
p is correct with respect to its specification, all suffixes of
the computations of p also satisfy the specification
Methods for proving program correctness:
Sequence of states
•
•
A state is a fixpoint of p iff no action of p is enabled in that state
An action of p preserves S iff executing the action,
starting from any state where the action is enabled and S holds,
yields a state where S holds
Recall the Hoare-triple notation: {S} ac {T},
where S and T are state predicates of p, ac is an action of p
{S} ac {T} means that starting from any state where S holds,
execution of ac upon termination yields a state where T holds
Method for proving program correctness:
Sequence of states
Observe:
- {S} ac {true} is always true
- {S} ac {false} is never true
- {false} ac {S} is always true
- {S} ac {S} iff ac preserves S
Closed
•
S is closed in p iff each action of p preserves S
 We will use the abbreviation
{S} p {T} for (ac : ac  p : {S} ac {T})
•
Observe:
- S is closed in p iff {S} p {S}
- true is closed in p is always true
- false is closed in p is always true
The temporal modality closed is used to prove safety properties
Leads-to
•
•
S leads-to R in p iff each computation of p that starts
at a state where S holds eventually reaches a state
where R holds
Observe:
- leads-to is reflexive: T leads-to T
- leads-to is transitive: if T leads-to S and S leads-to R,
then T leads-to R
•
The temporal modality leads-to is used to prove progress
properties
Leads-to (contd.)
•
•
If S is closed, one way to prove S leads-to R in p
is in terms of a variant function
A variant function is a mapping from the state space of p
to a set W that is well-founded under a relation <
 A set W is well-founded under <
iff every <-chain of W-elements is finite
 A <-chain is one where the successor of every element
in the chain is < the element
•
To prove S leads-to R, show that at any state where S holds,
either R holds or executing any action of p decreases the value
of the variant function
Since the variant function value cannot decrease infinitely, it
follows that eventually a state is reached where R holds
Proofs of Program Correctness
•
•
•
To simplify the proof of program correctness, we distinguish
one state predicate as the invariant of p
S is a invariant of p iff S is closed and every computation of p
that starts at a state where S holds satisfies the specification
Observe:
 Since the invariant S is closed, it holds at all states
in all computations of p that start at states where S holds
 Thus, S characterizes the set of all states
that p reaches from some set of states
 It follows that reachability analysis is one way
of calculating the invariant
Proofs of Program Correctness (contd.)
•
Observe:
 Not every state predicate that is closed in p needs to
hold at states where the invariant holds; e.g. false
 The proofs of correctness -of safety and of liveness-
are carried out with respect to the invariant
•
In some case, "auxilliary" (or "thought") variables have to
be added to a program to define its invariant
Proof of programs (sequential)
Example 0 :
program EUCLID
invariant :
variant function :
gcd(x,y) = gcd(X,Y)
(x max y) +
or
x+y+
{
{
1 if xy  ox
0 if x=y  o=x
1 if xy  ox
0 if x=y  o=x
Proof of programs (sequential)
Example 1 : program BBSORT
invariant :
x is a permutation of INIT_x
 0 j  m  k  N

(n : 0  n < j : x.n  x.(n+1)  n=N-1)

(n : k  n < j : x.m  x.n)

(n,l : 0  n < j  j  l < N : x.n  x.l)
variant function :
 N-j , N-k 
Proof of programs (sequential)
Example 2 : program HYSORT
invariant :
x is a permutation of INIT_x
variant function :
( j : 0  j < N : N-j  X.j )
Alternative Model for Proving Program Correctness:
Sequence of actions
•
Let b and c be actions of p
•
We say b commutes over c iff
the effect of executing b followed by c is identical to
the effect of executing c followed by b