1
$\begingroup$

In C.A.R Hoare's Communicating Sequential Processes (1978), he presents the SQUASH problem:

Replace every pair of consecutive asterisks "**" by an upward arrow "↑". Assume that the final character input is not an asterisk.

The given solution is:

X :: *[c:character; west?c →
  [c ≠ asterisk → east!c
   ▯c = asterisk → west?c;
     [c ≠ asterisk → east!asterisk; east!c
      ▯c = asterisk → east!upward arrow
]]]

He then challenges the reader to adapt this process to deal with input that ends in an odd number of asterisks.

It seems that this can be done by making the second west?c an alternative command, such that if getting next input from west fails, we output c to east:

X :: *[c:character; west?c →
  [c ≠ asterisk → east!c
   ▯c = asterisk → [west?c;
     [c ≠ asterisk → east!asterisk; east!c
      ▯c = asterisk → east!upward arrow
     ▯east!c
]]]]

Is this correct? Is there a better solution?

$\endgroup$
1
  • $\begingroup$ Have you tried proving that your solution works? This is how we usually check whether are solutions are correct. $\endgroup$ Aug 25 '17 at 10:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.