[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Curl, multiple inheritance, and interfaces (was Re: cheerful static typing)

Disclaimer: the software I'm about to describe is *not* mine, but it is in
development within the research group that I work for. I'll try to avoid
blatant misrepresentation, but any mistakes in my description are my own,
and should not be held against my employer.

There's a system developed by the Kestrel Institute called Specware, which
is based around the concept of specifications as logical theories, which can
be composed and refined to build concrete systems. It uses a functional
specification language which borrows from ML and Haskell, but adds syntactic
support for defining axioms, conjectures, and transformations between

So, to borrow the 'stack' model, you could write code that looked like the

spec Stack is
    op push : Stack * Any -> Stack
    op pop : Stack -> Stack * Any
    op top : Stack -> Stack * Any

    axiom pushThenPopIsIdentity is
        fa(s : Stack, t : Stack, x : Any)
            push(s, pop(push(t, x))) = push(s, x)

    axiom topReturnsLastPushed is
        fa(s : Stack, x : Any)
            top(push(s, x)) = x

This kind of high-level spec can then be refined, for example, in one that
implements the operations using a list as the concrete internal data
structure, and the system will determine proof obligations arising from the
refinement. Those obligations that can be discharged programatically (using
one of several automated theorem provers) are, and then the user is asked to
assist in finding solutions for the remainder.

It's definately *not* a "lightweight language" -- it's strongly, statically
typed, has only fledgling support for describing stateful behavior, and the
type system would probably seem extremely esoteric to anyone but a
mathematician. However, for those who "get it", (which usually doesn't
include me) it can be a very powerful tool for capturing the semantics of a
program specification in a machine-understandable (and check-able) way.

If this seems interesting to anyone, I suggest you browse some of the papers
on Kestrel's tech transfer page:


Now, back to the tools that are fun to hack with...

Lennon Day-Reynolds
Software Engineer
Kestrel Institute