This is the Z Specification Language, see:
http://directory.google.com/Top/Computers/Programming/Languages/Z/

Personally, I prefer Maude - http://maude.cs.uiuc.edu/ - which is
executable (inherently), reflective, and dynamic.

On Fri, 15 Aug 2003, Alan Kay wrote:

> Thanks Daniel --
>
> Do you have any pointers to this?
>
> Cheers,
>
> Alan
>
> -----
>
> At 5:05 PM +0000 8/15/03, daniel.a.joyce at att.net wrote:
> >Nasa uses such a system that takes programs specified in Z-code ( A
> >combination language / logical constraint system to prove program correctness
> >) and generates code from that...

-- 
Brian T. Rice
LOGOS Research and Development
http://tunes.org/~water/