보호 명령어

Guarded Command Language

GCL(Guarded Command Language)은 술어 트랜스 [1]시멘틱스에 대해 Edsger Dijkstra에 의해 정의된 언어입니다.프로그램이 실용적인 프로그래밍 언어로 작성되기 전에 프로그래밍 개념을 간략하게 결합합니다.Hoare 로직을 사용하여 프로그램의 정확성을 쉽게 입증할 수 있습니다.

가드 명령어

보호 명령어는 보호 명령어의 가장 중요한 요소입니다.보호 명령어에서는 이름 그대로 명령어는 "보호"됩니다.가드는 명제이며, 이는 스테이트먼트가 실행되기 전에 참이어야 합니다.그 진술이 실행될 때, 누군가는 가드가 사실이라고 가정할 수 있다.또한 가드가 false일 경우 해당 문장은 실행되지 않습니다.보호 명령어를 사용하면 프로그램이 사양을 충족하는지 쉽게 확인할 수 있습니다.그 진술은 종종 또 다른 경계 명령이다.

구문

보호 명령어는 G → S 형식의 명령문입니다.

  • G는 경비대라고 불리는 제안입니다.
  • S는 스테이트먼트입니다.

G가 참일 경우 보호 명령어는 단순 S로 작성해도 된다.

의미론

계산에서 G가 마주치는 순간 평가된다.

  • G가 참일 경우 S를 실행합니다.
  • G가 false일 경우 콘텍스트를 보고 처리 방법을 결정합니다(어떤 경우에도 S를 실행하지 마십시오).

건너뛰고 중지하다

Skip 및 Abort는 매우 단순할 뿐만 아니라 보호된 명령어로 중요한 문장이기도 합니다.Abort는 정의되지 않은 명령입니다.무엇이든 해 주세요.abort 문은 종료할 필요도 없습니다.증명을 작성할 때 프로그램을 설명하는 데 사용되며, 이 경우 대개 증명이 실패합니다.건너뛰기는 빈 명령입니다. 아무것도 하지 마십시오.이것은 구문이 문을 필요로 하지만 프로그래머가 기계가 상태를 변경하는 것을 원하지 않을 때 프로그램 자체에서 사용됩니다.

구문

건너뛰다. 
중단하다

의미론

  • 건너뛰기: 아무것도 하지 않음
  • 중단: 모든 작업을 수행합니다.

과제

변수에 값을 할당합니다.

구문

v : = E

또는

v0n, v1, ..., vn:= E0, E1, ..., E

어디에

  • v는 프로그램 변수입니다.
  • E는 대응하는 변수와 같은 데이터 타입의 식입니다.

연결

문은 세미콜론(;) 1개로 구분됩니다.

선택: if

선택 항목(종종 "conditional statement" 또는 "if statement"라고 함)은 실행할 명령어가 선택되는 보호 대상 명령어 목록입니다.여러 개의 가드가 참일 경우 1개의 문이 비결정적으로 실행되도록 선택됩니다.어느 가드도 참이 아닌 경우 결과는 정의되지 않습니다.적어도 1개의 가드가 참이어야 하므로 종종 빈 문 "건너뛰기"가 필요합니다.

구문

G0 → S0 G1 → S1일 경우...Gn → Sn fi

의미론

선택 실행 시 모든 가드를 평가한다.어느 가드도 true로 평가되지 않으면 선택 실행이 중단됩니다.그렇지 않으면 값이 true인 가드 중 하나가 비결정적으로 선택되고 대응하는 문이 실행됩니다.[2]

예

간단하죠.

의사 코드:

a < b일 경우 c를 True로 설정하고 그렇지 않을 경우 c를 False로 설정합니다.

보호 명령어: 

a < b → c : = true a ≥ b → c : = false fi일 경우

스킵 사용

의사 코드:

오류가 True이면 x를 0으로 설정합니다.

보호 명령어: 

오류 = 참 → x : = 0 오류 = 거짓 → fi 건너뛰기

두 번째 가드가 생략되고 오류 = False일 경우 결과는 중단됩니다.

더 많은 가드 참

a ≥ b → max : = a a a a a → max : → b fi인 경우

a = b이면 a 또는 b가 최대값의 새 값으로 선택되며 결과는 동일합니다.그러나, 이것을 실장하고 있는 사람은, 어느 쪽이 다른 쪽보다 쉽거나 빠르다고 생각할 수 있습니다.프로그래머에게 차이가 없기 때문에 어느 쪽이든 자유롭게 구현할 수 있습니다.

반복: 실행

이 반복은 가드가 모두 참이 될 때까지 가드의 명령을 반복적으로 실행합니다.보통, 경비원은 한 명뿐입니다.

구문

G0 → S0 G1 → S1...Gn → Sn od

의미론

반복 실행 시 모든 가드를 평가한다.모든 가드가 false로 평가되면 건너뛰기가 실행됩니다.그렇지 않으면 값이 true인 가드 중 하나가 비결정적으로 선택되고 해당 문이 실행된 후 반복이 다시 실행됩니다.

예

원래의 유클리드 알고리즘

a, b : → A, B. a < b → b : = b - a < a → a - b od 를 실행합니다.

이 반복은 a = b일 때 끝나며, 이 경우 a와 b는 A와 B의 최대 공약수를 갖는다.

Dijkstra는 이 알고리즘에서 두 개의 무한 사이클을 동기화하는 방법을 확인합니다.a := a - b그리고.b := b - a그런 식으로a≥0그리고.b≥0진실인 채로 남습니다.

확장 유클리드 알고리즘

a, b, x, y, u, v:= A, B, 1, 0, 0, 1; do b 0 0 → q, r:= a div b, mod b; a, b, x, y, v:= b, r, u, x - q*u, y - qv od

이 반복은 b = 0일 때 끝나며, 이 경우 변수는 베주트의 항등식에 대한 해: xA + yB = gcd(A,B)를 유지한다.

비결정론적 정렬

a>b → a, b : = b, b > c → b, c : = c, b c> d → c, d : → d, c od 를 실행합니다.

프로그램은 그 중 하나가 후속 요소보다 큰 동안 계속 요소를 허용합니다.이 비결정론적 버블 정렬은 결정론적 버전보다 효율적이지는 않지만 증명하기 쉽습니다. 요소가 정렬되지 않는 동안에는 중지되지 않으며 각 단계에서 최소 2개의 요소를 정렬합니다.

아르그 최대

x, y = 1, 1 do x4n → f(y) → x := x+1 f(x) → f(y) → y := x; x := x+1 fi od인 경우

이 알고리즘은 특정 정수 함수 f가 최대인 값 1 µ y µ n을 찾습니다.연산뿐만 아니라 최종 상태도 반드시 고유하게 결정되는 것은 아니다.

적용들

구조별 프로그램 수정

가드 명령의 관측적 일치성을 격자로 일반화하면 정제 [3]미적분학으로 이어집니다.이는 B-Method와 같은 Formal Method에서 기계화되어 있으며, 이를 통해 명세서에서 프로그램을 정식으로 도출할 수 있습니다.

비동기 회선

가드된 명령어는 다른 명령어 선택에 대해 임의의 상대 지연을 허용하기 때문에 준지연 비감응 회로 설계에 적합합니다.이 응용 프로그램에서는 회선 내의 노드 y를 구동하는 로직게이트는 다음과 같은2개의 가드명령어로 구성됩니다.

PullDownGuard → y : = 0 PullUpGuard → y : = 1

여기서 PullDownGuard와 PullUpGuard는 로직 게이트의 입력 기능으로, 게이트가 출력을 각각 끌어내리거나 끌어올리는 시기를 설명합니다.기존의 회로 평가 모델과 달리 일련의 가드 명령어(비동기 회로에 대응)에 대한 반복은 해당 회로의 가능한 모든 동적 동작을 정확하게 설명할 수 있습니다.전기 회로 소자에 대해 기꺼이 따르는 모델에 따라 보호 명령어에 대한 추가 제한이 있어야 보호 명령어에 대한 설명이 완전히 충족될 수 있습니다.일반적인 제약사항으로는 안정성, 비간섭성 및 자가 무효화 [4]명령어 부재 등이 있습니다.

모델 체크

가드 명령은 SPIN 모델 체커에서 사용되는 Promela 프로그래밍 언어 내에서 사용됩니다.SPIN은 동시 소프트웨어 응용 프로그램이 올바르게 작동하는지 확인합니다.

다른.

Perl 모듈명령어:Guarded는 Dijkstra의 보호 명령어에 결정적이고 올바른 변형을 구현합니다.

레퍼런스

  1. ^ Dijkstra, Edsger W. "EWD472: Guarded commands, non-determinacy and formal. derivation of programs" (PDF). Retrieved August 16, 2006.
  2. ^ Anne Kaldewaij (1990), Programming: The Derivation of Algorithms, Prentice Hall
  3. ^ Back, Ralph J (1978). "On the Correctness of Refinement Steps in Program Development (Phd-Thesis)" (PDF). Archived from the original (PDF) on 2011-07-20.
  4. ^ Martin, Alain J. "Synthesis of Asynchronous VLSI Circuits".