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

  • Backend: Chalice
  • Language: PVL
  • Features: Witnesses
  • Path to Example File: manual/witness.pvl
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 30 (comments not included)
  • Lines of Specification: 12 (40.0% of total)
  • Computation Time: 9.2 seconds