Array properties

is example show how to prove functional properties about the contents of arrays using notation that avoids the problem with functions ensuring quantified properties about quantified permissions.

General Information

  • Backend: Silicon
  • Language: PVL
  • Features: Sequences, Arrays
  • Path to Example File: manual/array.pvl
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 28 (comments not included)
  • Lines of Specification: 15 (53.6% of total)
  • Computation Time: 36.4 seconds