Pcal, procedures and tests

[fl]

 

Hi all,

 

1 - Can we have a macro that returns a macro? I suppose no.

 

2 - In pcal the variables generated by the parameters of the procedures appears after the macros, it is unfortunate.

 

3 - Suppose I want to develop an algorithm  with pcal under toolbox . There are several procedures. I want to test each procedure

with a model before testing the main algorithm. There is no simple way to have models that do that I think. I mean we can't have

a model that tests a procedure, another model that tests another procedure and eventually a model that tests the main algorithm.

 

--

FL

[Leslie Lamport]

Hi Frederic,

   1 - Can we have a macro that returns a macro? I suppose no.

I don't understand this, because macros don't "return" anything.
Perhaps what want a macro uses another macro.  This is allowed,
as long as the macro being used precedes the macro using it.

 
   2 - In pcal the variables generated by the parameters of the
       procedures appears after the macros, it is unfortunate.

I don't understand this, because the variables I believe you are
talking about are part of the TLA+ translation, and the macros are in
the PlusCal source.

   3 - Suppose I want to develop an algorithm with pcal under toolbox .
       There are several procedures.  I want to test each procedure with a
       model before testing the main algorithm.  There is no simple way to
       have models that do that I think.  I mean we can't have a model that
       tests a procedure, another model that tests another procedure and
       eventually a model that tests the main algorithm.

I don't know of any programming language that lets you test a
procedure; they only let you test a program that calls the procedure.
If you describe how you would do what you want for procedures in a
program, perhaps we can figure out how it should be done in PlusCal.

Cheers,

Leslie

[fl]

   1 - Can we have a macro that returns a macro? I suppose no.

I don't understand this, because macros don't "return" anything.

I wanted a macro like:

 

   Macro(a,b) = Test(x) == x.out = a /\ x.in = b

 

 

That way I could write later:

 

   SelectSeq(u, Macro(1,2))

 

 
   2 - In pcal the variables generated by the parameters of the
       procedures appears after the macros, it is unfortunate.

I don't understand this, because the variables I believe you are
talking about are part of the TLA+ translation, and the macros are in
the PlusCal source.

 

 

The translation generates:

 

Variables x, y, z

 

A == ...

 

B == ..

 

Variables a, b, c (* a b c are procedures parameters*)

 

I think it would be better if we had

 

Variables x, y, z, a, b, c

 

A == ...

B == ..

Because that way one can use a b c in the macros.

 

 

I don't know of any programming language that lets you test a
procedure; they only let you test a program that calls the procedure.

 

It is often unfortunate by the way. Because definitely we often needs to test procedure in isolation.

 

Obvioulsy there are workaround. That's true. But it's not as good.

 

Thank you, Leslie, for your comments.

 

--

FL

[fl]

 

Macro(a,b) = Test(x) == x.out = a /\ x.in = b

 

I mean:

 

Macro(a,b) == Test(x) == x.out = a /\ x.in = b

 

--

FL

[Stephan Merz]

   1 - Can we have a macro that returns a macro? I suppose no.

I don't understand this, because macros don't "return" anything.

I wanted a macro like:

 

   Macro(a,b) = Test(x) == x.out = a /\ x.in = b

 

 

That way I could write later:

 

   SelectSeq(u, Macro(1,2))

I do not understand what you intend but this must be wrong. You can only pass expressions as arguments to operators (such as SelectSeq), whereas you seem to intend your Macro to produce a definition. Definitions are not expressions in TLA+.

Secondly, I do not understand the example because SelectSeq is a ternary operator, and the second and third argument are expected to be integers whereas the right-hand side of your Test operator is a Boolean expression.

Best regards,

Stephan

[fl]

 

Hi Stephan,

 

I do not understand what you intend but this must be wrong. You can only pass expressions as arguments to operators (such as SelectSeq), whereas you seem to intend your Macro to produce a definition. Definitions are not expressions in TLA+.

 

Well I will check but I'm pretty sure you can pass a macro to SelectSeq.

 

Secondly, I do not understand the example because SelectSeq is a ternary operator, and the second and third argument are expected to be integers whereas the right-hand side of your Test operator is a Boolean expression.

 

 

 

I think you are confusing SelectSeq and SubSeq. SelectSeq is binary and takes a macro.

 

http://research.microsoft.com/en-us/um/people/lamport/tla/summary.pdf

 

--

FL

[fl]

 

3 - Suppose I want to develop an algorithm  with pcal under toolbox . There are several procedures. I want to test each procedure

with a model before testing the main algorithm. There is no simple way to have models that do that I think. I mean we can't have

a model that tests a procedure, another model that tests another procedure and eventually a model that tests the main algorithm.

 

 

An idea that might solve this problem. The models are kept in their own subdirectories. And a copy of the thaplus specification

is  copied in these directories every time the model is activated.

 

Well suppose some models can be declared as frozen. No fresh copy of the specification would replace the old one. That

way one might test a procedure (calling it in the main algorithm) and then proceed further with the specification and

once every procedure is developped with its own specification in its frozen model subdirectorie, we might develop the

main algorithm with its own (non-frozen) models. 

 

--

FL

[Stephan Merz]

My bad, excuse me. You want to write the following:

  Test(a,b,x) == x.out = a /\ x.in = b

and then use it as in

  SelectSeq(u, LAMBDA x : Test(1,2,x))

It might be tempting to write

  Test(a,b) == LAMBDA x : ...

  SelectSeq(u, Test(1,2))

but the TLA+ syntax does not allow you to do that (see Section 16.4 of the Hyperbook).

Regards,

Stephan

[fl]

  SelectSeq(u, LAMBDA x : Test(1,2,x))

 

Nice! that's exactly what I want. I had not yet used the LAMBDA feature. It is a good opportunity to do that.

 

--

FL

[Leslie Lamport]

Hi Frederic,

Each model is stored in a separate directory, along with the version
of the spec on which it was last run.  And models can be locked.
However, I don't see the use of essentially keeping a separate copy of
each procedure in a model since, if testing the entire algorithm
reveals that a procedure needs to be changed, you'd want to change
that copy as well.

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, I have no reason to believe that it will be useful
enough to warrant adding it to the Toolbox.  Especially when there are
so many other things that we'd like to do if we had the time.

Leslie

[fl]

 

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 call

any 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 to

call any function in isolation easily I think because of the stack system

and eventually embedded languages like lua make it possible to call procedure in isolation as well.

 

--

FL

[Leslie Lamport]

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

[fl]

[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

[Leslie Lamport]

Hi Frederic,

   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.

The only good reason to write a library module to aid model checking
is to define operators that TLC can't handle (except perhaps at
exorbitant computation cost) without overriding the definition with
Java code.  For example, it seems to be impossible to define Seq so
that TLC can evaluate the expression seq \in Seq(Nat) when seq is a
sequence.  For example, there was no need for the standard Bags
module.

The problem of writing a sorting operator that TLC can evaluate
efficiently is discussed in Section 9.2 of the Hyperbook.  The
definition given there is five lines long.  The time-complexity of
that algorithm is O(n^2).  If you need a more efficient algorithm, you
could find one in an algorithm book somewhere and code it as a
recursively defined TLA+ operator.  But if O(n^2) isn't good enough,
you are probably using TLA+ to do things it wasn't meant to do.

One of the differences between programming and specification is that
re-use is not an issue.  If you want to re-use something you've
defined elsewhere, copy-and-paste is good enough.  (Imagine what
programming would be like if no one wrote programs longer
than 2000 lines.)  The operator defined in the Hyperbook sorts a set
of records according to a 'key' field, because that's what was needed
in the example of Section 9.  If this was programming, I'd have
written a sorting procedure to handle any sorting task, involving
callbacks to compute the sorting keys.  But there's no need for that
for a definition I can write in 5 lines.  If I needed to sort a
sequence of integers, I could just copy the definition from the
HyperBook and modify it in a straightforward way.

Leslie