Option types

In this verification example several properties on option types are asserted. Note that `None` cannot be type checked. Type inference is needed and is only implemented for assignment (`=`), and the equality operators (`!=` and `==`).

General information

ID97
Articlenone
Back-endSilicon
LanguagePVL
FeaturesOption types
Sources
Path to example filemanual/option.pvl
Date2017-06-20

Statistical information

Lines of code16 lines (comments not included)
Lines of specification4 lines (25% of the total)
Computation time5178 milliseconds

Example code

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