Precondition and Guard in Classic B

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 END is equal to if 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 - d is not feasible since 0 >= 1 is 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: NAT violated if we assume the MININT and MAXINT is -1 and 3 separately
  • dec(-1) will cause Precondition d: NAT & n >= d violated
  • dec(1), dec(2) and dec(3) will cause Precondition d: NAT & n >= d violated as well

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