Next: JML to BML Compiler, Previous: Encoding of BML in Class File Format, Up: Top
Link with BCV .
There is not much written down about this. In the preliminary design of BML paper, Section 3.2 contains some example typechecking rules. Mariela's thesis contains a bit more, but they are not fundamentally different.
Basic typechecking 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 typechecking including checking of object subtyping is not implemented.