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

  • Backend: Silicon
  • Language: Java
  • Features: Witnesses
  • Path to Example File: witnesses/Getters.java
  • Should Verify: Yes
  • Date: 2017-06-21
  • Lines of Code: 58 (comments not included)
  • Lines of Specification: 32 (55.2% of total)