Sha256: 57c99840390b4e8a58003c9babb8087510bfac6dc520243faa857b4c25a2f60c
Contents?: true
Size: 463 Bytes
Versions: 7
Compression:
Stored size: 463 Bytes
Contents
{{!
Define correctness predicates.
Correctness predicates may refer operators defined in 'operators'.
In order to activate invariant add INVARIANT directive in 'correcness.cfg'
For example:
\* When 'PetStore_ValidatePet' is defined in 'operators'
\* All pets in 'v_pets' should be valid
PetStore_ValidatePets == \A pet \in v_pets: PetStore_ValidatePet( pet )
}}
{{!>correctness_pet_name.tla}}
{{!>correctness_types.tla}}
Version data entries
7 entries across 7 versions & 1 rubygems