Used internally.
Used internally.
Returns all postconditions merged into a single function
A postcondition is a function that takes three parameters, s0, s1 and r.
A postcondition is a function that takes three parameters, s0, s1 and r. s0 is the abstract state before the command was run, s1 is the abstract state after the command was run, and r is the result from the command's run method. The postcondition function should return a Boolean (or a Prop instance) that says if the condition holds or not. You can add several conditions to the postConditions list.
Returns all preconditions merged into a single function
A precondition is a function that takes the current abstract state as parameter and returns a boolean that says if the precondition is fulfilled or not.
A precondition is a function that takes the current abstract state as parameter and returns a boolean that says if the precondition is fulfilled or not. You can add several conditions to the precondition list
Use 'postConditions += ...' instead.
Use 'postConditions += ...' instead.
Use 'preConditions += ...' instead.
Abstract commands are defined as subtypes of the traits Command or SetCommand. Each command must have a run method and a method that returns the new abstract state, as it should look after the command has been run. A command can also define a precondition that states how the current abstract state must look if the command should be allowed to run. Finally, we can also define a postcondition which verifies that the system under test is in a correct state after the command exectution.