| An example of a class with a temporal property. This class
implements a simple vote manager. When an instance of this class is
created, we specify how many ballots we have. Users can call
voteYes or voteNo. The manager will manage the counting. There is
also a method to stop the counting.
We want a temporal specification that says:
[]!open && numberOfBallots=N ==> []numberOfBallots=N
That is, once the counting is stopped, the number of ballots still
left in the manager should not change anymore. This property is
implemented as a never-claim automaton, coded in the class
invariant.
|
