success (library)

Usage and interface

Documentation on exports

Usage:get_success_info(Call,SgKey,Sg,Sv,AbsInt,Prime,PatternsApplied)

Given a call pattern for an imported predicate defined by Call call and Sg abstract substitution, Prime is the success substitution resulting from the application of the success policy for imported predicates. PatternsApplied is instatiated to no if there are no applicable patterns.

  • The following properties should hold at call time:
    (nonvar/1)Call is currently a term which is not a free variable.
    (nonvar/1)SgKey is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Sv is currently a term which is not a free variable.
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (var/1)Prime is a free variable.
    (var/1)PatternsApplied is a free variable.

Usage:succ_pattern(SuccessPolicy,AbsInt,Sg,Call,Succ)

Provides on backtracking the call and success patterns Call and Succ of exported predicates of a given goal Sg on a given abstract domain AbsInt. It uses SuccessPolicy to check which marked patterns can be used.

This predicate is called by the analysis procedure to get info about imported predicates. For performance reasons, when an external predicate of an imported module is requested, all the exported predicates of the imported module are loaded into memory.

  • The following properties should hold at call time:
    (nonvar/1)SuccessPolicy is currently a term which is not a free variable.
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (var/1)Call is a free variable.
    (var/1)Succ is a free variable.

Usage:apply_success_policy(SuccessPolicy,AbsInt,SgKey,Sg,Sv,Proj,Patterns,Prime,PatternsApplied)

Applies the success policy given as first argument to the list of triples (SgProj,Proj,Succ) Patterns w.r.t. Proj. If there are no applicable patterns in Patterns, it returns either '$bottom' or the topmost substitution, depending on the type of the success policy (either it is underapproximating or overapproximating, respectively.) PatternsApplied is instatiated to no if there are no applicable patterns.

  • The following properties should hold at call time:
    (nonvar/1)SuccessPolicy is currently a term which is not a free variable.
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)SgKey is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Sv is currently a term which is not a free variable.
    (nonvar/1)Proj is currently a term which is not a free variable.
    (nonvar/1)Patterns is currently a term which is not a free variable.
    (var/1)Prime is a free variable.
    (var/1)PatternsApplied is a free variable.

Documentation on imports

This module has the following direct dependencies: