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

Re: Pcal, procedures and tests

[Replacing procedures by their specifications]

  You write a specification of what the system is
supposed to do.  You then implement that specification as a set of
components, showing that if each of the components satisfies its
specification, then their combination satisfies the system's
specification.  You then implement each component, knowing that if
each component meets its specification, then the system meets its

Obviously it is a good idea. I dare say it is even The Idea.

The only downside is that TLC favors algorithms over CHOICE or even recursion. But it deserves
to be tried.

A solution might be to have a library of boosted specifications. For example a specification of a
sorting algorithm but with a piece of code behind to speed up TLC.