Tutorial Model Checking, Proof and CBC: Difference between revisions
(Created page with ' We assume that you have completed Tutorial Complete Model Checking.') |
No edit summary |
||
| Line 1: | Line 1: | ||
We assume that you have completed [[Tutorial Complete Model Checking]]. | |||
Let us examine the following B machine: | |||
<Pre> | |||
MACHINE DoubleCounter | |||
VARIABLES counter | |||
INVARIANT | |||
counter:NATURAL & counter<=128 | |||
INITIALISATION counter:=1 | |||
OPERATIONS | |||
Double = PRE counter<100 THEN counter := 2*counter END; | |||
Halve = BEGIN counter := counter/2 END | |||
END | |||
</Pre> | |||
Now click the "Model Check" button. After a short while, ProB will give you the following message: | |||
[[file:ProBModelCheckNoCounterExampleFound.png|center]] | |||
Revision as of 11:01, 1 March 2011
We assume that you have completed Tutorial Complete Model Checking.
Let us examine the following B machine:
MACHINE DoubleCounter VARIABLES counter INVARIANT counter:NATURAL & counter<=128 INITIALISATION counter:=1 OPERATIONS Double = PRE counter<100 THEN counter := 2*counter END; Halve = BEGIN counter := counter/2 END END
Now click the "Model Check" button. After a short while, ProB will give you the following message:
