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

  • Backend: Chalice
  • Language: Java
  • Features: Lists
  • Path to Example File: predicates/minmax-list.pvl
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 33 (comments not included)
  • Lines of Specification: 8 (24.2% of total)
  • Computation Time: 10.6 seconds