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

ID88
Articlenone
Back-endSilicon
LanguagePVL
FeaturesArrays, Sequences
Sources
Path to example filemanual/array.pvl
Date2017-06-20

Statistical information

Lines of code28 lines (comments not included)
Lines of specification15 lines (53.57% of the total)
Computation time36405 milliseconds

Example code

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