25 May
2024
25 May
'24
11:36 p.m.
Another Gypsy user here...
For KSOS-11 the kernel was described in SPECIAL - as a set of axioms and
theorems. There was no actual connection between the formal specification
in SPECIAL and the Modula code.
Some of the critical user-space code for a trusted downgrade program, to
bridge data from higher levels of classification to lower, was written in
Gypsy. I visited UT Austin and Dr Good(?)'s team to learn it, IIRC. Gypsy
was considered better in that the specification was tied to the executable
through the pre/post conditions - and the better support for semi-automated
theorem proving.
On Sat, May 25, 2024 at 10:18 AM Paul Winalski <paul.winalski(a)gmail.com>
wrote:
On Fri, May 24, 2024 at 8:18 PM Bakul Shah via TUHS
<tuhs(a)tuhs.org> wrote:
At one point I had suggested turning Go's Interface type to something like
Guttag style abstract data types in that relevant
axioms are specified
right in the interface definition. The idea was that any concrete type that
implements that interface must satisfy its axioms. Even if the compiler
ignored these axioms, one can write a support program that can generate a
set of comprehensive tests based on these axioms. [Right now a type
"implementing" an interface only needs to have a set of methods that
exactly match the interface methods but nothing more] The underlying idea
is that each type is in essence a constraint on what values an instance of
that type can take. So adding such axioms simply tightens (& documents)
these constraints. Just the process of coming up with such axioms can
improve the design (sor of like test driven design but better!).
At one point I worked with a programming language called Gypsy that
implemented this concept. Each routine had a prefix that specified axioms
on the routine's parameters and outputs. The rest of Gypsy was a
conventional procedural language but the semantics were carefully chosen to
allow for automated proof of correctness. I wrote a formal specification
for the DECnet session layer protocol (DECnet's equivalent of TCP) in
Gypsy. I turned up a subtle bug in the prose version of the protocol
specification in the process.
-Paul W.