This file show how the syntax for stating that an object is an instance of a specific class (\typeof) works. It is future work to make sure that the knowledge that this is an instance of C is automatically added.
Path to example file
Lines of code
14 lines (comments not included)
Lines of specification
5 lines (35.71% of the total)
Note, verification may take a while and has a time-out of 20 seconds.