Table ASMs

  • Colin Campbell ,
  • Yuri Gurevich

Formal Methods and Tools for Computer Science (Proceedings of Eurocast 2001) eds. R. Moreno-Diaz and A. Quesada-Arencibia, Universidad de Las Palmas de Gran Canaria Canary Islands, Spain |

Ideally, a good specification becomes the basis for implementing, testing and documenting the system it defines. In practice, producing a good specification is hard.

Formal methods have been shown to be helpful in strengthening the meaning of specifications but despite their power, few development teams have successfully incorporated them into their software processes. This experience indicates that producing a usable formal method is also hard.

This paper is the story of how a particular theoretical result, namely the normal forms of Abstract State Machines, motivated a genuinely usable form of specification that we call ASM Tables.

We offer it for two reasons. The first is that the result is interesting in and of itself and — it is to be hoped — useful to the reader. The second is that our result serves as a case study of a more general principle, namely, that in bringing rigorous methods into everyday practice, one should not follow the example of Procrustes: we find that it is indeed better to adapt the bed to the person than the other way round.

We also offer a demonstration that an extremely restricted syntactical form can still contain sufficient expressive power to describe all sequential machines.

To read this publication, click on the images below: