wysiib/plspec

plspec's Issues

Improve "Spec Not Found" Error

Recursive specs (as e.g. one_of) might not trigger a "spec not found" exception if, you guessed it, the spec was not found.

Improve Code Quality

• Rename some predicates to be more descriptive. Some issues are:
  • spec_predicate_recursive: not really recursive from a user perspective
  • take auxfrom the auxiliar predicates
  • spec_and and and
  • or and or2
• Better module structure
  • too much interleaving
  • make them smaller?
• More Tests
  • test coverage not high enough
  • check more scenarios

Allow to Disable Term Expansion

custom types -- examples

Hello,

I noticed plspec and am trying to get my head around using it in my prolog program. I am in particular interested in creating custom types, such as a custom type for an Internal ID and a custom type for a human readable label-- both are atoms.

Can this be done? If yes, are there examples?

thank you,

Dan

Recognizing recursive structures?

Consider the following spec:

:- defspec(tree(X), one_of([compound(node(tree(X), X, tree(X))),
                            atom(empty)])).

Now if you call valid(X, node(empty, 1, empty)), you want to get as results for X:
tree(int), tree(atomic), tree(integer) and tree(number),
But at the moment you also get results like
compound(node(tree(int), int, tree(int)), compound(node(atom(empty), integer, atomic)) and other combinations.

For node(node(empty,1,empty), 1, node(empty,1,empty)) you get over 40000 results instead of the 4 desired.

It would be great to recognize these recursive structures and stop there.

plspec should take advantage of module information

Either term expansion magic or explicitly stating the module in all calls to plspec.

Allow Naming of Arguments

Consider this code snippet:

generate(true, true, X) :- (...).
generate(false, true, X) :- (...).
generate(true, false, X) :- (...).

A valid spec might be:

:- defspec(boolean, one_of([compound(true), compound(false)])).
:- spec_pre(generate/2, [boolean, boolean, var]).

However, one still does not associate a meaning with these parameters (what is true or false?).
Thus, in order to improve the documentation aspect of plspec, it would make sense to allow (or enforce?) additional syntax in order to name parameters, e.g.:

:- spec_pre(generate/2, [should_do_foo:boolean, should_do_bar:boolean, result:var]).

Coroutines should terminate

Specs might wrongly get rid of singleton warnings

pls fix

Improve Error Messages

A proper error message should include:

• the smallest sub-term that does not match a spec
• the position in the argument vector
• the predicate that was called
• the entire argument vector and all specs (?)

which_posts is not working as intended

Consider the following (spec'd) predicate:

:- spec_post(my_member/2, [list(X), var], [list(X), X]).
my_member([H|_], H).

Then, assume the query my_member([1,2,3],X).

Expected behaviour: the post condition is selected to be checked later on.
Actual behaviour: the unification of H in my_member happens before the which_posts check occurs, therefore H is not bound to the variable X but rather to the value 1. Thus, the post condition is discarded.
Suggested fix: switch ordering of which_posts and the unification with the head of the clause if possible. This has to modify the term expander.

Improve error messages

• values in one_of should not be repeated
• source of error should be clear (spec_pre, spec_invariant,..)

Add Error Handler

Allow to register an error handler that is used instead of throw(_). This should allow to report multiple spec violations in the same run.