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