Package org.sosy_lab.java_smt.test.ultimate

Class ProcedureContract<E,​V>

  • Type Parameters:
    E - The type of expressions
    V - The type of variables
    public class ProcedureContract<E,​V>
extends Object
    A contract specifying the behaviour of a procedure (in Boogie or the ICFG) or function (in C).

    The behaviour is specified using up to three kinds of clauses:

    1. A "requires" clause specifies a precondition that must hold before a call.
    2. An "ensures" clause specifies a relation guaranteed to hold between the state before the call and the state at the procedure exit.
    3. Optionally, a "modifies" clause specifies a subset of global variables that the procedure may write to. Writes to any other global state is forbidden.
    Author:
    Dominik Klumpp (klumpp@informatik.uni-freiburg.de)

    • Constructor Detail

      • ProcedureContract

        public ProcedureContract​(String procedure,
                         E requires,
                         E ensures)
        Creates a new contract that does not have a "modifies" clause, i.e., the contract specifies that the procedure may arbitrarily modify global state as long as it satisfies the "ensures" clause.
        Parameters:
        procedure - The procedure for which a contract is being created
        requires - The "requires" clause. A value of null represents a trivial clause, i.e., the logical formula true.
        ensures - The "ensures" clause. A value of null represents a trivial clause, i.e., the logical formula true.

      • ProcedureContract

        public ProcedureContract​(String procedure,
                         E requires,
                         E ensures,
                         Set<V> modifies)
        Creates a new contract with a "modifies" clause, i.e., the contract specifies that the procedure may only modify the given global variables.
        Parameters:
        procedure - The procedure for which a contract is being created
        requires - The "requires" clause. A value of null represents a trivial clause, i.e., the logical formula true.
        ensures - The "ensures" clause. A value of null represents a trivial clause, i.e., the logical formula true.
        modifies - The set of global variables modifiable by the procedure.

    • Method Detail

      • hasModifies

        public boolean hasModifies()

      • getProcedure

        public String getProcedure()

      • getRequires

        public E getRequires()

      • getEnsures

        public E getEnsures()

      • getModifies

        public Set<V> getModifies()

      • hasOnlyTrivialClauses

        public boolean hasOnlyTrivialClauses()
        Determines whether both the "requires" and "ensures" clauses of the contract are null, i.e., represent the logical formula true, and the contract does not have a "modifies" clause.

        Note that this does not mean that the entire contract is trivial in the sense that any procedure would satisfy it, as a "requires" clause of true indicates that there can be no assertion failure during execution of the procedure for any input or initial global state. An entirely trivial contract would thus instead need to have a "requires" clause false.

        For contracts with "modifies" clauses this method always return false as there is no way to determine if the "modifies" clause is trivial without knowing the entire set of global variables in the program: only when every variable can be modified, the clause would be trivial.