On 28-Feb-1999, Carl R. Witty <[EMAIL PROTECTED]> wrote:
>
> I downloaded the NU-Prolog manual and skimmed it, but I didn't see the
> features you're describing (probably because I haven't "done" Prolog
> since my learn-5-languages-in-a-quarter class 12 years ago). Could
> you give me a pointer to which section of the manual I should read?
I'm not sure if it is documented in the NU-Prolog manual.
It's probably documented somewhere, but off-hand I don't know where.
Anyway the relevant feature is `where' annotations on `:- pred'
declarations and `:- type' declarations.
For example:
:- pred append(list(T), list(T), list(T))
where (X, Y, Z : length(X, XL), length(Y, YL), length(Z, ZL),
plus(XL, YL, ZL)).
This gives a partial specification for `append'; it states that
append(X, Y, Z) should succeed only if the length of X plus the
length of Y is equal to the length of Z.
You can also attach conditions to types, e.g.
:- type sorted_list(T) == list(T) where X : sorted(X).
Then when you write
:- pred merge(sorted_list(T), sorted_list(T), sorted_list(T)).
it is equivalent to
:- pred merge(list(T), list(T), list(T)) where
(X, Y, Z : sorted(X), sorted(Y), sorted(Z)).
> For Eiffel, as far as I can tell, what you get are assertions in
> function declarations (pre- and post-conditions on the functions).
You also get class invariants.
> Consider the Haskell function sortBy:
>
> > sortBy :: (a -> a -> Ordering) -> [a] -> [a]
>
> Suppose you wanted to verify that the output of sortBy was sorted
> according to the supplied comparison function. [...]
> It must be a precondition on sortBy that the comparison function
> satisfies this constraint. This can be expressed as a precondition,
> if preconditions can have universally quantified formulas (so
> preconditions can no longer be executable).
>
> Now, when you define a sorting function, you want to state and verify
> the above property. Where does it go?
Eiffel doesn't have higher-order functions, so the first argument
of sortBy would be a class with a sort method. The requirement
that the sort method be an ordering would be a class invariant
of this class.
> To me, the set of "acceptable comparison functions" feels like a type,
> so "encoding" this requirement in the type system is natural.
It's certainly reasonable to consider class invariants in Eiffel
or `where' annotations in NU-Prolog to be a part of the type.
The point is that they are a _clearly separated_ part of the type.
--
Fergus Henderson <[EMAIL PROTECTED]> | "Binaries may die
WWW: <http://www.cs.mu.oz.au/~fjh> | but source code lives forever"
PGP: finger [EMAIL PROTECTED] | -- leaked Microsoft memo.
