Hi Frederic,
You're right; I wasn't thinking. The Java debugger allows one to
execute any method that's callable in the current context. Debuggers
are based on executing code one step at a time. You can't do that in
TLC. Instead, you can start TLC in any state by specifying the
appropriate Init predicate. So you can check any procedure by
starting in an initial state in which control is at the beginning of
the procedure. Of course, if you want to execute the procedure by a
single process in a multi-process algorithm, you'll have to change the
next-state action.
Debugging a procedure by itself makes sense in programming. But it
doesn't make much sense testing the procedure inside a debugger,
manually entering each input. Instead, one writes a "harness"--a
program that calls the procedure repeatedly and checks its output.
You can do that just as well in PlusCal by making each harness a
separate spec.
However, PlusCal isn't a programming language; it's much more
expressive than any programming language. I wonder if you're not
taking advantage of that. It sounds like you're writing a procedure
to compute a value. Why are you doing that rather than just writing a
TLA+ operator that computes the value and using the operator in an
_expression_ in the PlusCal algorithm? If you're using PlusCal to help
you write a program, then you can write a separate little PlusCal
algorithm that implements the computation of the operator.
Breaking a program into procedures is a method of hierarchical
decomposition. You write and test the separate parts, then write and
test the program that combines the parts. This is a bottom up
procedure. If you find out that combining the parts doesn't work, you
have to re-implement some of the parts and try again. TLA+ allows you
to work top-down. 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. The downside of the top-down approach is that it's
possible that you discover you're unable to implement a component that
satisfies its spec, so you have to re-do your high-level
implementation. Preventing that looping requires the engineering
skill to know what you can implement. Preventing looping in a
bottom-up development requires the much rarer ability of being able to
figure out in your head how a collection of components are going to
work when put together.
Maybe you should be working top-down instead of bottom-up.
Leslie
On Saturday, April 11, 2015 at 5:14:40 AM UTC-7, fl wrote:
Anyway, all programming languages have some form of procedure. If no
one has thought it important enough to add such a feature to their
debugging tools,It is not exactly true I think. For example in the GNU C debugger it is definitely possible to callany procedure (with great difficulties obviously because of the parameters and the global variables).For some languages such as Haskell it is intrinsically possible to test any function in isolation.For languages such as Forth the system of stacks make it possible tocall any function in isolation easily I think because of the stack systemand eventually embedded languages like lua make it possible to call procedure in isolation as well.--FL