chc.api.ContractAssumption module

Assumption on the return value of a function represented by a predicate.

Assumptions about return values of functions are never ‘imposed’ like those on function arguments by the receiving function. The reason is that different functions may have different expectations about the postcondition of a function, or the transfer relation of the function.

Necessary postconditions may be suggested with the open proof obligation as a hint towards conditions that can then be imposed deliberately via a contract assumption.

class chc.api.ContractAssumption.ContractAssumption(capi: CFunctionApi, id: int, callee: int, xpredicate: XPredicate, ppos: List[int], spos: List[int])[source]

Bases: object

Post condition assumption or assumption on global variable.

Parameters

  • capi (CFunctionApi) – the function api of the function that requests the assumption

  • id (int) – identification number of the assumption

  • callee (int) – (local) id of the function for which the postcondition is requested (-1 for a request on a global variable)

  • xpredicate (XPredicate) – predicate representing the assumption

  • ppos (List[int]) – id’s of the primary proof obligations that require this assumption for discharge

  • spos (List[int]) – id’s of the supporting proof obligations that require this assumption for discharge

property callee: int
property capi: CFunctionApi
property id: int
property ppos: List[int]
property spos: List[int]
property xpredicate: XPredicate