The differences between Precondition and Guard in B machine.
Precondition
Preconditioned substitution (termination)
- \( P \mid S \) called \( P \) pre \( S \):
PRE P THEN S END- The operation is only activated when P holds. Otherwise, it may result in an incorrect behaviour.
- \( [P \mid S]R \Leftrightarrow (P \land [S]R) \)
- If \( P \) doesn't hold, the operation is not guaranteed to achieve anything, say \( R \), since \( P \land [S]R \) never holds whatever \( R \). This substitution which is not able to establish anything is said to be non-terminating substitution
Guard
Guarded substitution (feasibility)
- \( P \Longrightarrow S \) called \( P \) guards \( S \)
- \( S \) is performed under the assumption \( P \)
- \( [ P \Longrightarrow S]R \Leftrightarrow (P \implies [S]R) \)
- If \( P \) holds, post-condition \( R \) is established. Otherwise, if \( P \) is false, \( [ P \Longrightarrow S] \) can establish anything. It's said to be non-feasible.
Differences
\( P \) doesn't hold
- \( P \mid S \) can not establish anything if \( P \) doesn't hold. When \( P \) doesn't hold, the substitution is said to abort. (Like the divergence in CSP)
- \( P \Longrightarrow S \) can establish anything if \( P \) doesn't hold. When \( P \) doesn't hold, the substitution is not feasible.
Postcondition
- In order to establish the post-condition, \( P \mid S \) must prove \( P \) but \( P \Longrightarrow S \) may assume \( P \).
Substitution
- In \( P \mid S \), \( P \) is assumption, which is a contract between the user of the operations and the machine providing the operations
- In \( P \Longrightarrow S \), \( P \) is condition for the substitution \( S \) to be feasible.
IF P THEN S END. For example,IF 0 < n THEN n := n - 1 ENDis equal toif 0 < n then n := n - 1 else n := n end
Example and Demonstration
An example
MACHINE
PreGuardTest
VARIABLES
n
INVARIANT
n: NAT
INITIALISATION
n := 0
OPERATIONS
inc(i) = PRE
i: NAT
THEN
n := n + i
END;
dec0(d) = BEGIN
n := n - d
END;
dec(d) = PRE
d: NAT & n >= d
THEN
n := n - d
END;
decp(d) = SELECT d: NAT & n >= d THEN
n := n - d
END;
dec1(d) = BEGIN
IF n >= d THEN
n := n - d
END
END;
dec2(d) = BEGIN
SELECT n > d THEN
n := n - d
WHEN n = d THEN
n := n - d
ELSE
n := n
END
END
END
Demonstration with ProB
default PRE as SELECT
- Precondition will be treated as guard
- when n=0, call dec1(1) will cause invariant voilented.
- when n=0, dec(1) is not enabled since the precondition doesn't hold. So long as decp(1)
- when n=0, call dec1(1) won't change the value of n since the substitution
n := n - dis not feasible since0 >= 1is false - when n=0, dec2 works like dec1
default PRE as SELECT is false
- Precondition will be treated as precondition
- just after initialisation, ProB state window showed
- inc(-1) will cause Precondition
i: NATviolated if we assume the MININT and MAXINT is -1 and 3 separately - dec(-1) will cause Precondition
d: NAT & n >= dviolated - dec(1), dec(2) and dec(3) will cause Precondition
d: NAT & n >= dviolated as well
- inc(-1) will cause Precondition
Proof Obligations
References
- J.-R. Abrial, The B-book: assigning programs to meanings. Cambridge University Press, 2005.
- Ken Robinson, An Introduction to the B Method Preconditions and Guards, 2001
