Witnesses: Getters

This example shows how to use getters in combination with the witness encoding of predicates with arguments. When calling the tool on this file, the verification result should be a _Pass_.

General information

ID162
Articlenone
Back-endChalice
LanguageJava
FeaturesWitnesses
Sources
Path to example filewitnesses/Getters.java
Date2017-06-21

Statistical information

Lines of code58 lines (comments not included)
Lines of specification32 lines (55.17% of the total)
Computation timeunknown

Example code

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