Sha256: bd964d5e32d564a046eb4a09f711ecbb7bcd23ac8ecefb9590c79187a803d3c9
Contents?: true
Size: 687 Bytes
Versions: 7
Compression:
Stored size: 687 Bytes
Contents
{{!
Assumption predicates (and possibly operators), and ASSUME directive.
For example:
\* True iff 'field' in records in 'set' have correct 'domain'
Assume_DomainOfAField( set, field, domain ) == { p[field] : p \in set } = domain
\* Verify that domain of named field is correct
Assume_Pet_Domains == Assume_DomainOfAField( t_Pet, "id", d_id )
\* Domain verification phase 1
ASSUME Assume_Pet_Domains
}}
{{>assumption_generic.tla}}
\* Defintion domains
{{>assumption_address_domains.tla}}
{{>assumption_owner_domains.tla}}
{{>assumption_tag_domains.tla}}
{{>assumption_pet_domains.tla}}
{{>assumption_id_domains.tla}}
{{>assumption_domains.tla}}
Version data entries
7 entries across 7 versions & 1 rubygems