[m-dev.] Re: assertions (was: Assocative predicates)
David Glen JEFFERY
dgj at cs.mu.OZ.AU
Fri Apr 24 14:48:49 AEST 1998
On 24-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> On Fri, 24 Apr 1998, David Glen JEFFERY wrote:
> > > Perhaps the valid_term syntax will need to be
> > > broadened to make it possible to refer to instances of the type parameters
> > > of the instances of the class.
> > I think you can get the same effect by making assertions about type class
> > methods and having the compiler (or theorem prover, or whatever) check that
> > assertion about that method for each instance declaration.
> Right, but you still can't specify invariants about the types themselves.
> I can't think of any good examples at the moment; here's the best I can
> think of. You might have a non_negative_number type class, with all the
> usual operations, each with all the usual assertions. But you'd still want
> to assert that every element of every type in the class is >= 0.
Ah yes, I think you're right. (Although to make your example more plausible,
the invariant would be that for every value, >= zero holds, where zero is
a function of the type class).
love and cuddles,
David Jeffery (dgj at cs.mu.oz.au) | Marge: Did you just call everyone "chicken"?
MEngSc student, | Homer: Noooo. I swear on this Bible!
Department of Computer Science | Marge: That's not a Bible; that's a book of
University of Melbourne | carpet samples!
Australia | Homer: Ooooh... Fuzzy.
More information about the developers