Sha256: c3050c3a4fc7450c0c3664ef85c09b4b0ed4e729fe1c9b44c618272367f9296f
Contents?: true
Size: 575 Bytes
Versions: 7
Compression:
Stored size: 575 Bytes
Contents
{{!
Correctness predicates.
Correctness predicates may refer operators defined in 'operators'.
In order to activate invariant add INVARIANT directive in 'correcness.cfg'
For example:
\* When 'ValidatePet' is defined in 'operators'
\* All pets in 'v_pets' should be valid
ValidatePets == \A pet \in v_pets: ValidatePet( pet )
}}
{{>correctness_type_invariants.tla}}
{{>correctness_pet_name.tla}}
{{>correctness_unique_pet.tla}}
{{>correctness_unique_tag.tla}}
{{>correctness_ref_tag.tla}}
{{>correctness_coherent_owner_address.tla}}
Version data entries
7 entries across 7 versions & 1 rubygems