package linksem
-
linksem_zarith
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type expression = | Var0 of string(*Ranges over memory addresses
*)| Const of Nat_big_num.num(*Fixed memory address
*)
The type expression denotes addresses, whether known or to be ascertained.
type value_formula = | VFTrue| VFFalse| VFBinaryRelation of binary_relation * expression| VFBinaryConnective of binary_connective * value_formula * value_formula| VFNot of value_formula
type memory_image_formula = | MIFTrue| MIFFalse| MIFExists of string * memory_image_formula| MIFBinaryRelation of binary_relation * expression * expression| MIFBinaryConnective of binary_connective * memory_image_formula * memory_image_formula| MIFAssertValueFormula of expression * value_formula| MIFNot of memory_image_formula
val mk_range : Nat_big_num.num -> Nat_big_num.num -> value_formula