Types

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 int, float, bool and str are supported:

class State:
    def __init__(self):
        self.i : int = 0
        self.s : str = "Hello world"
        self.b : bool = True

Apart from these, you can define own enumeration and record types and use defaultdict dictionaries with typed keys and values.

Enums

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.

from enum import Enum, unique
@unique
class Hand(Enum):
    rock     = 1
    paper    = 2
    scissors = 3

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.

class State:
    def __init__(self):
        self.hand : Hand = Hand.rock

Records

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.

from typing import NamedTuple
class Vector3D(NamedTuple):
    x : int
    y : int
    z : int

Such records/named tuples can be positionally instantiated by calling the class constructor:

class State:
   def __init__(self):
      self.v : Vector3D = Vector3D(0,0,1)

The record fields can be accessed by name:

def receive_IncX(self):
    self.v: Vector3D = Vector3D(self.v.x + 1, 0, 1)

Dictionaries

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:

from collections import defaultdict
from typing import Dict

class State:
    def __init__(self):
        self.mymap : Dict[int,int] = defaultdict(lambda:0, {1:1, 2:4})
    def receive_Add(self, x : int):
        self.mymap[x] : int = x * x