Imandra needs the static type information to reason about the model python code. You must supply the type hints when writing the model.
Currently, four basic built-in types
str are supported:
Apart from these, you can define own enumeration and record types and use
defaultdict dictionaries with typed keys and values.
Enumerations can be created by subclassing
Enum standard library class. The class can only contain a list of identifiers for the individual enumeration cases. We also require the enum identifiers to start with lowercase characters.
Notice that you must assign the numeric values for the enumeration cases. We require that the
@unique decorator is always applied to the class so that no duplicate values are supplied.
The custom enum can then be referenced normally and used in the type hints.
Records are declared by subclassing
NamedTuple class from the
typing standard module. The class can only contain a list of record fields with their corresponding types.
Such records/named tuples can be positionally instantiated by calling the class constructor:
The record fields can be accessed by name:
Formal reasoning about dictionaries requires certain constraints imposed on them: all the keys and all the values must be of the same type and a default value (returned if the key is absent from the dictionary) must be provided. We use collections.defaultdict standard collection as a base for such dictionaries. The required type hint for such dictionaries must be supplied with a typing.Dict generic type hint: