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.
Path to example file
Lines of code
33 lines (comments not included)
Lines of specification
8 lines (24.24% of the total)
Note, verification may take a while and has a time-out of 20 seconds.