[프로그래밍 언어론] Statement - Level Control Structure Part 4 - Guarded Commands

* Guarded Commands ( Dijkstra 1975 )
 - 목적 : 프로그램을 개발하면서 검증을 바로바로 하고 싶다.
  > 즉, 프로그램 개발이 끝난 동시에 검증이 끝나있음을 의미 한다.
 - 위의 목적을 이루기 위해서 selection과 loop를 새로 정의 하였다.

* Selection of Guarded Command
  

  -  []의 역할
   > 일반 if-elseif문에서의 elseif와 같은 기능을한다. 그러나 여기엔 크나큰 차이가 있다.

   > 일반 if-elseif문과 다르게 모든 boolean expression에 대해서 T/F를 검사를 하여 True인 것 중에서 랜덤으로

      하나의 stmt를 실행한다.

   > 조건이 모두 false이면 error를 출력해준다.

  - []의 기능으로 인한 이점 
   > 랜덤으로 하나를 실행한다 : 알아서 해당하는 모든 경우에 대해서 test를 실시한다.
   > 조건이 모두 false면 error를 출력해준다 : 프로그래머가 생각하지 못한 경우가 존재하는 것을 알려준다.
  ex) if x>=y -> max := x 
       [] x<=y -> max := y
        fi                  
        // 같을 경우를 생각해보자.
        // 우리가 일반적인 selection에서는=라는 것은 둘 중에 하나에 만 표시를 한다.
        // 이는 증명의 용의성을 떨어뜨린다.
        // 즉, Guarded Command를 사용하므로써 증명의 용의성을 제공해준다. 

* Loop of Guarded Command 
 

 
 - selection과 마찬가지로 모든 boolean expression의 T/F를 판단하여, T중 랜덤하게 하나를 실행한다.  
 - T인 경우가 존재하는 경우엔 계속하여 Loop를 돈다. 
 - selection과 차이점으로 모두 false라면 Loop를 종류한다.
  ex) 3개의 수를 정렬  
  do a1 > a2 -> temp = a1; 
                      a1 = a2; 
                      a2 = temp; 
  [] a2 > a3 -> temp = a2; 
                      a2 = a3; 
                      a3 = temp;  
  od 
  // 모두가 F일때 loop이 종류가 된다면, a1 <=  a2 <= a3가 성립하게 정렬됬음을 의미한다.