Friday, 6 December 2013

Precondition and Guard in Classic B

The differences between Precondition and Guard in B machine.

Precondition

Preconditioned substitution (termination)

  • PS 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.
    • [PS]R(P[S]R)
    • If P doesn't hold, the operation is not guaranteed to achieve anything, say R, since P[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)

  • PS called P guards S
    • S is performed under the assumption P
    • [PS]R(P[S]R)
    • If P holds, post-condition R is established. Otherwise, if P is false, [PS] can establish anything. It's said to be non-feasible.

Differences

P doesn't hold

  • PS 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)
  • PS 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, PS must prove P but PS may assume P.

Substitution

  • In PS, P is assumption, which is a contract between the user of the operations and the machine providing the operations
  • In PS, 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

No comments :

Post a Comment