Program transformation

We would like to be able to write an obviously correct implementation of an algorithm in Concurrent Programming Languages and then mechanically transform the program into one with identical behaviour, but more efficient performance. Other things that program transformation may help us to look at include: By ;SPM_quot;mechanical transformation;SPM_quot; is meant a transformation, selected from some bag of tricks by the programmer or a clever program, which can then be applied mechanically, and which is known to produce a precisely equivalent program. The problem lies, of course, in selecting and proving the bag of tricks, and in deciding how to use them on a particular program. We now wish to show that a given Process satisfies a specification. This is done by proofs! Combining the spec for GAME, and subtracting OutCome from both sides of both inequalities:

#equation1057#

or writing length(trace(PROC) event as tr event:

#equation1059#

Now if P sat S and S =;SPM_gt; T, P sat T. i.e. if a spec S implies a spec T, then everything satisfying S must satisfy the (weaker) T. Now (induction!):

Assume some process X satisfies #tex2html_wrap_inline4110# InCoin - tr #tex2html_wrap_inline4114# then (InCoin #tex2html_wrap_inline4116# OutCome #tex2html_wrap_inline4118# X) satisfies

#equation1067#

or

#equation1069#

This implies GAME does satisfy spec since:

#equation1071#

and

#equation1073#

and

#equation1075#

implies

#equation1077#

  • Note, STOP satisfies every spec that can be satisfied by any process.
  • Note, any process defined only using prefix, choice and guarded recursion never stops.