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.