8 Type Checking BML

[Jacek]

Link with BCV .

There is not much written down about this. In the preliminary design of BML paper, Section 3.2 contains some example type checking rules. Mariela's thesis contains a bit more, but they are not fundamentally different.

Basic type checking is also done in the BMLlib library. The types of formulas and expressions are checked (e.g. that the assertion is always a boolean formula etc.) As of now, the advanced type checking including checking of object subtyping is not implemented.

Some collected remarks from text about type checking: BML tools still have to check explicitly that all predicates are side-effect-free.

to allow calls to static methods, the grammar allows identifiers as primary-expr. Type checking will enforce that these are class names.

Can we write type checking rules for expressions?

To do: check BCV description and check which rules are applicable to BML