Predicates: Min-max list

Verifying a min/max list: a linked list of integers with all integers in a certain range (where the range is determined by some `min` and `max`). The property of being a min/max list is captured as a pure function `minmax`. We verify that a fresh list is a min/max list when inserting a variable within some range.

General information

ID131
Articlenone
Back-endChalice
LanguageJava
FeaturesLists
Sources
Path to example filepredicates/minmax-list.pvl
Date2017-06-20

Statistical information

Lines of code33 lines (comments not included)
Lines of specification8 lines (24.24% of the total)
Computation time10631 milliseconds

Example code

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