Guarded Command

Guarded Commands
• Suggested by Dijkstra ปี 1975
• Purpose: to support a new programming methodology that supported verification (correctness) during development
• Basis for two linguistic mechanisms for concurrent programming (in CSP and Ada)
• Basic Idea: if the order of evaluation is not important, the program should not specify one

Selection Guarded Command
• Form
if ->
[] ->
...
[] ->
fi
fi เป็นการจบด้วยการ reverse word
• Semantics: when construct is reached,
– Evaluate all Boolean expressions
– If more than one are true, choose one non-deterministically
– If none are true, it is a runtime error (ถ้าเป็น false ทั้งหมดจะเกิด runtime eror)

If I = 0 - > sum := sum +i
[] i > j - > sum := sum + j
[] j >I - > sum := sum +i

*ถ้า if = 0 และ j > I โครงสร้างจะเลือก nondeterminate ระหว่างการกำหนดค่าที่ 1 กับ 3


Loop Guarded Command
• Form
do ->
[] ->
...
[] ->
od
• Semantics: for each iteration
– Evaluate all Boolean expressions
– If more than one are true, choose one non-deterministically; then start loop again
– If none are true, exit loop



Guarded Commands: Rationale
• Connection between control statements and program verification is intimate
• Verification is impossible with goto statements
• Verification is possible with only selection and logical pretest loops
• Verification is relatively simple with only guarded commands


อันนี้อ่านแล้วยังงง ๆ ไว้อ่านใหม่ :
http://www.ipl.t.u-tokyo.ac.jp/~hu/pub/teach/msp06/lec2.pdf