Re: Pcal, procedures and tests

[fl <freder...@xxxxxxxxxxx>]

[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
specification.

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.

-- 

FL