Completing CSP
Bill Roscoe ( OUCL )
- 11:30 13th February 2008 ( week 5, Hilary Term 2008 )Oxford University Computing Laboratory, Room 347
After adding a natural new operator to CSP that is related to interrupt, we are able to show that no further operator can be required. Specifically, we define what it means for an operator to have a CSP-like operational semantics, and show that every such operator is expressible using the extended language.
A side benefit of this is that it becomes possible to define new operators operationally, confident that they have congruent definitions over the semantic models and fit naturally into CSP's refinement framework.