plspec_core

Imports	Exports
	Name: enable_all_spec_checks/0 Name: enable_spec_check/1 Name: spec_pre/2 Name: spec_post/3 Name: spec_invariant/2 Name: defspec/2 Name: defspec_pred/2 Name: defspec_pred_recursive/4 Name: defspec_connective/4 Name: valid/2 Name: set_loglevel/1 Name: log/3 Name: asserted_spec_pre/5 Name: asserted_spec_invariant/3 Name: asserted_spec_invariant/4 Name: asserted_spec_post/7 Name: check_predicate/1 Name: set_error_handler/1

Imports

Exports

Name: enable_all_spec_checks/0

Name: enable_spec_check/1

Name: spec_pre/2

Name: spec_post/3

Name: spec_invariant/2

Name: defspec/2

Name: defspec_pred/2

Name: defspec_pred_recursive/4

Name: defspec_connective/4

Name: valid/2

Name: set_loglevel/1

Name: log/3

Name: asserted_spec_pre/5

Name: asserted_spec_invariant/3

Name: asserted_spec_invariant/4

Name: asserted_spec_post/7

Name: check_predicate/1

Name: set_error_handler/1

Predicates

Predicates:

:/2

expansion/12

Description:
newargs: only relevant if head implements pattern matching:
log(debug, 'These pre-post specs matched: ~w', [PrePostSpecs]),
log(debug, 'Unified the arguments with ~w', [Args]),

expansion(Head, Body, PreSpecs, PreSpecTypes,
    InvariantSpecOrEmpty, InvSpecTypes,
    PrePostSpecs,PrePostSpecTypes, PostSpecs, PostSpecTypes,
    NewHead, NewBody) :-
    Head =.. [Functor|Args],
    length(Args, Lenny),
    %% newargs: only relevant if head implements pattern matching:
    % consider foo(foo). then the call 'foo(bar)' would not violate the spec but only fail
    % thus, we insert a fresh variable and check the unification with the argument term later on
    length(NewArgs, Lenny),
    NewHead =.. [Functor|NewArgs],
    NewBody = (% determine if at least one precondition is fulfilled
    (PreSpecs = [] ->
    true
    ;
    (plspec:plspec_some(
    spec_matches(NewArgs, true),
    PreSpecs,
    PreSpecTypes
    ) ->
    true
    ;
    plspec:error_not_matching_any_pre(
    Functor/Lenny,
    NewArgs,
    PreSpecs
    )
    )
    ),
    (InvariantSpecOrEmpty = [InvariantSpec] ->
    InvSpecTypes = [InvSpecType],
    lists:maplist(
    plspec:setup_uber_check(Functor/Lenny,InvSpecType),
    InvariantSpec,
    NewArgs
    )
    ;
    true
    ),
    % gather all matching postconditions
    plspec:which_posts(
    PrePostSpecs,
    PrePostSpecTypes,
    PostSpecs,
    PostSpecTypes,
    Args,
    ValidPrePostSpecs,
    PostsToCheck,
    PostTypesToCheck),
    %% log(debug, 'These pre-post specs matched: ~w', [PrePostSpecs]),
    % unify with pattern matching of head
    NewArgs = Args,
    %% log(debug, 'Unified the arguments with ~w', [Args]),
    Body,
    lists:maplist(
    plspec:check_posts(Args),
    ValidPrePostSpecs,
    PostsToCheck,
    PostTypesToCheck
)
).

should_expand/4

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_plspec_runtime_checks,true)
* Non-determinate: plspec_core:should_expand/4 (clause 1)
* Calls nondet predicate plspec:check_predicate/1 .
* Non-determinate: plspec_core:do_expand/3 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: plspec_core:do_expand/3 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: plspec_core:do_expand/3 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: plspec_core:do_expand/3 (clause 4)
* Indexing cannot distinguish this from clause 5.
* Non-determinate: plspec_core:do_expand/3 (clause 5)
* Indexing cannot distinguish this from clause 6.
* Non-determinate: plspec_core:do_expand/3 (clause 6)
* Indexing cannot distinguish this from clause 8.
* Non-determinate: plspec_core:do_expand/3 (clause 8)
* Indexing cannot distinguish this from clause 9.
* Non-determinate: user:term_expansion/2 (clause 1)
* This predicate is multifile, and this clause has no cut.
* Non-determinate: user:term_expansion/6 (clause 1)
* This predicate is multifile, and this clause has no cut.

Name: do_expand/3	Module: plspec_core
Name: prolog_load_context/2
Name: log/3	Module: foo_error

Name: expansion/12	Module: plspec_core
Name: findall/3
Name: log/3	Module: foo_error
Name: !
Name: should_expand/4	Module: plspec_core

Name: true
Name: asserted_spec_post/7	Module: plspec
Name: ->/2
Name: asserted_spec_invariant/3	Module: plspec
Name: ->/3
Name: asserted_spec_pre/5	Module: plspec
Name: functor/3
Name: check_predicate/1	Module: plspec

Name: =/2
Name: =../2
Name: length/2