GCs (cont.)

อ่านอันนี้เข้าใจขึ้น http://en.wikipedia.org/wiki/Guarded_Command_Language

In pseudocode:

if a < b then c := True
else c := False

In guarded command language:

if a < b c := true
[] a ≥ b c := false
fi

Skip and Abort
Skip and Abort are very simple as well as important statements in the guarded command language. Abort is the undefined instruction: do anything. The abort statement does not even need to terminate. It is used to describe the program when formulating a proof, in which case the proof usually fails. Skip is the empty instruction: do nothing. It is used in the program itself, when the syntax requires a statement, but the programmer does not want the machine to change states.

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

KU 2009

insert image testing.

photo by Ms.Usa Sammapun

first blog

....................