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

• Backend: Silicon
• Language: PVL
• Features: Option types
• Path to Example File: manual/option.pvl
• Should Verify: Yes
• Date: 2017-06-20
• Lines of Code: 16 (comments not included)
• Lines of Specification: 4 (25.0% of total)
• Computation Time: 5.2 seconds