Witnesses: Predicates

This example shows how reasoning with explicit witnesses works. It is supposed to work with Chalice, but the assertions are not proven.

General information

ID176
Articlenone
Back-endChalice
LanguageJava
FeaturesWitnesses
Sources
Path to example filewitnesses/predicates.pvl
Date2017-06-21

Statistical information

Lines of code50 lines (comments not included)
Lines of specification25 lines (50% of the total)
Computation timeunknown

Example code

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