Witness encoding

This short verification example shows how witness encodings work. This program verifies using Chalice. Witnesses are less needed in Silver, since predicates may have arguments in Silver. However, witnesses still should be used with magic wands.

General information

ID100
Articlenone
Back-endChalice
LanguagePVL
FeaturesWitnesses
Sources
Path to example filemanual/witness.pvl
Date2017-06-20

Statistical information

Lines of code30 lines (comments not included)
Lines of specification12 lines (40% of the total)
Computation time9238 milliseconds

Example code

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