cpcogan — 2004-12-30 22:31:51

Can we analyze for correctness? In general, no.

But the range of programs that we can analyze for correctness by
mechanical means is not just "toy" programs.

By constraining the development tools in certain ways, we can make
programs that are both powerful and yet mechanically verifiable in a
reasonable time by software.

I don't mean that we can test for correctness in the sense of: Does
it do what we want it to, but rather in the sense of: Is it, as it
stands, a complete and logically coherent piece of software. This
means testing that all references are satisfiable, that all
recursions can end, that each defined component is defined according
to mathematically-describable rules on the basis of previously-
defined entities.

James Martin wrote about this, in _System Design from Provably
Correct Constructs_ (Prentis-Hall, 1985). The method he describes
used non-standard control construct equivalents, and started from a
set of mathematically-defined primaries. The design software was
graphical (trees) and, after verification, code was generated
completely mechanically (mechanical generation of source, alone,
eliminates coding errors).

All the data available within a control construct equivalent had to
be explicitly stated, and it had to be explicitly divided into input
and output (and the same item could never be both an input and an
output). Each data item was dynamically assigned a value once and
once only, so they weren't variables in the ordinary sense (though
the same name could be assigned another variable in a separate
execution, of course).

The three basic control construct thingies could be used to define
more-complex construct thingies, so the method wasn't as restrictive
as it might seem at first.

Anyway, the point is that the various restrictions at the
foundational level led to a method that led to designs that were
provably correct (in a logical/mathematical sense, not necessarily in
a correct-for-the-problem sense), and this in turn enabled complete
code to be generated mechanically.

The question is: Can we do something similar with Joy or one of the
other of our various languages? Because of the way we can "package"
control constructs and such, it would seem that we are well on the
way towards just such a mechanically-checkable tool. What the method
described above had that our languages don't is mainly static
parameter-and-type checking.

What I'm wondering is: Can we add a mechanism that allows for static
checking in those cases where we *want* it, without having this same
mechanism get in our way when we want to do without it?

One thing that comes to mind is stack marking, and assertions for the
compiler. The assertions would tell the compiler how many and what
kinds of paramters are required. Stack marking would enable the
compiler to tell (in some case) whether there will be the right
number and types of parameters *for the given function* on the stack.
If all of our functions have statically-known stack effects, we can
have large stretches of code where a mechanical checker could work.

But what of functions that may take different numbers of items off
the stack and put different numbers of items back? Each time we
encounter such a function, our static code checker will fail until
some "clean" point is found later on (or outside of the caller,
perhaps, if it can be guaranteed to leave the stack in a statically-
known state).

Obviously, if we are going to do static checking for such cases, we
need something "smarter" than just paramter-counting and type-
checking. We need to have it analyze the code of the function that
has the "unstatic" behavior and see if *it* is correct. I think this
can actually be done (perhaps with another constraint or two). After
all, a function that pushes the integers 0 through N, given N, could
well be doing something we want, couldn't it? (we could have it
produce a list with the numbers in it, but the idea here is to do
correctness checking without restricting our way of handling the
stack).

It seems that this should all be possible, if all of the *primitives*
have fixed stack effects or if the stack effects are at least
generally describable to the checker.

I suppose it's possible that this degree of freedom in stack effects
would produce a combinatorial explosion of the same kind that makes
the general problem of program correctness effectively unsolvable for
any but the simplest programs. But, I'm hopeful that this would not
be the case, or that if it is, we could restrict uncheckability to
self-contained parts of our applications, so that overall correctness
could be checked *assuming* the correctness of these uncheckable
parts.

Ideas? Comments?

William Tanksley, Jr — 2004-12-30 23:11:56

On Thu, 30 Dec 2004 22:31:51 -0000, cpcogan <ccogan@...> wrote:

> By constraining the development tools in certain ways, we can make
> programs that are both powerful and yet mechanically verifiable in a
> reasonable time by software.

Yes -- SPARK ADA does this sort of thing to Ada. Very impressive, and
worth a read.

> What I'm wondering is: Can we add a mechanism that allows for static
> checking in those cases where we *want* it, without having this same
> mechanism get in our way when we want to do without it?

Here's a different question:

Can we design a language that can be /subsetted/ such that the subset
is both checkable and useful?

I think that's a more acheivable goal than designing a language that's
both safe AND never gets in the way of someone just wanting to hack
out code.

> One thing that comes to mind is stack marking, and assertions for the
> compiler. The assertions would tell the compiler how many and what
> kinds of paramters are required. Stack marking would enable the
> compiler to tell (in some case) whether there will be the right
> number and types of parameters *for the given function* on the stack.
> If all of our functions have statically-known stack effects, we can
> have large stretches of code where a mechanical checker could work.

You've read about strongForth, right? Its website is long gone, but
the wayback machine has it in its archives.

> Obviously, if we are going to do static checking for such cases, we
> need something "smarter" than just paramter-counting and type-
> checking. We need to have it analyze the code of the function that
> has the "unstatic" behavior and see if *it* is correct. I think this
> can actually be done (perhaps with another constraint or two). After
> all, a function that pushes the integers 0 through N, given N, could
> well be doing something we want, couldn't it? (we could have it
> produce a list with the numbers in it, but the idea here is to do
> correctness checking without restricting our way of handling the
> stack).

I can handle limiting iterations to be over arrays, but then we'd have
to deal with recursions; so your question seems to me to be
reasonable.

The theory of structured programming indicates that there should be
three ways to create variable stack effects: repetition, composition,
and alternation. "Repetition" refers to the effects of loops; it
happens when the same known stack effect happens an unknown number of
times. "Alternation" refers to the effect of conditionals; it happens
when there are two possible stack effects, only one of which will
actually happen. "Composition" is when you have multiple different
stack effects appearing one after the other; it happens in the process
of normal code and is usually easily handled, but when it appears
inside of a conditional block of code there must be some way to group
all of the stack effects together as one side of a conditional stack
effect.

> It seems that this should all be possible, if all of the *primitives*
> have fixed stack effects or if the stack effects are at least
> generally describable to the checker.

Recursion makes the first requirement impossible. I believe that being
able to describe the general effect using terms like the ones I use
above will solve the problem.

> I suppose it's possible that this degree of freedom in stack effects
> would produce a combinatorial explosion of the same kind that makes
> the general problem of program correctness effectively unsolvable for
> any but the simplest programs. But, I'm hopeful that this would not
> be the case, or that if it is, we could restrict uncheckability to
> self-contained parts of our applications, so that overall correctness
> could be checked *assuming* the correctness of these uncheckable
> parts.

I agree that this is extremely possible, and I'd love to see it (I'd
love to work on it, if I had time).

-Billy

Slava Pestov — 2004-12-31 01:40:45

cpcogan wrote:

> that all
> recursions can end,

This is not possible without using a non turing complete language!

> (mechanical generation of source, alone,
> eliminates coding errors).

But coding errors are easy to fix. Mechanical generation does nothing
for logic errors.

> But what of functions that may take different numbers of items off
> the stack and put different numbers of items back?

Do such functions matter?

> It seems that this should all be possible, if all of the *primitives*
> have fixed stack effects or if the stack effects are at least
> generally describable to the checker.

Have you played with Factor? It already does static stack checking. Only
the stack effects of primitives (170 or so) are entered manually; all
other stack effects are inferred. More than half of the words in the
library have a known stack effect.

Slava

Philippa Cowderoy — 2004-12-31 03:05:21

On Thu, 30 Dec 2004, Slava Pestov wrote:

>
> cpcogan wrote:
>> that all
>> recursions can end,
>
> This is not possible without using a non turing complete language!
>

However, it's worth asking whether there's a suitably useful subset of
turing complete available - for many use patterns there is, and certainly
being able to prove that a given piece of code lies within that subset
would be useful. Another idea that may prove useful is that some type
systems with subtyping (System F^ comes to mind) don't actually have a
notion of type-check failure, the equivalent concept being merely not
being able to say anything useful about a value ("it's somewhere in the
set of all possible values including non-termination").

--
flippa@...

Ivanova is always right.
I will listen to Ivanova.
I will not ignore Ivanova's recomendations.
Ivanova is God.
And, if this ever happens again, Ivanova will personally rip your lungs out!

William Tanksley, Jr — 2005-01-01 04:29:17

Philippa Cowderoy <flippa@...> wrote:

> On Thu, 30 Dec 2004, Slava Pestov wrote:
> > cpcogan wrote:
> >> that all
> >> recursions can end,

> > This is not possible without using a non turing complete language!

> However, it's worth asking whether there's a suitably useful subset of
> turing complete available - for many use patterns there is, and certainly
> being able to prove that a given piece of code lies within that subset
> would be useful.

That's also impossible in general -- but you're right, it's a good
thing, so the people at http://www.praxis-his.com/sparkada/ did it.
The trick is that although it's impossible for a Turing machine, it's
quite possible for a Turing machine with an oracle; thus, if you have
the programmer insert a little extra formal stuff into the comments,
your code can be classified.

The trick with SPARK Ada was:

1. Pick a language that was clearly and reasonably unambiguously
defined. Ada was chosen.

2. Choose a subset of it that's entirely invariant across all
platforms according to the specification. The result is called SPARK
Ada, in this case; some of the things that were NOT included were the
ability to use side effects in functions, multitasking, and dynamic
memory allocation.

3. Define a set of mandatory annotations that fit within comments and
allow the SPARK compiler to perform certain architectural analyses.

4. Design a set of proof annotations -- including preconditions,
postconditions, and so on -- that allow the SPARK theorem prover to
analyse the code for various conditions. Analyses may include maximum
stack depth, total exception freedom, total runtime freedom (there are
now Ada compilers that will generate a no-runtime-required image), and
so on.

> flippa@...

-Billy

Correctness-checking, type-checking, stack effects, constraints, etc.

cpcogan — 2004-12-30 22:31:51

William Tanksley, Jr — 2004-12-30 23:11:56

Slava Pestov — 2004-12-31 01:40:45

Philippa Cowderoy — 2004-12-31 03:05:21

William Tanksley, Jr — 2005-01-01 04:29:17