Using \instanceof and \typeof

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.

General information

ID157
Articlenone
Back-endSilicon
LanguageJava
Features
Sources
Path to example filetype-casts/TypeExample1.java
Date2017-06-21

Statistical information

Lines of code14 lines (comments not included)
Lines of specification5 lines (35.71% of the total)
Computation time20082 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.