[프로그래밍 언어론] Modeling Language Properties (4)

 

[4] Modeling Language Properties

Formal Properties of Languages
-  규칙에 의해 규정되는 언어와 이러한 언어의 인식에 관한 이론

Chomsky Hierarchy
-  Type 3 : Regular Grammars - Finite Automata
-  Type 2 : Context Free Grammars - (N) Pushdown Automata
-  Type 1 : Context Sensitive Grammars - Linear Bounded Automata
-  Type 0 : Unrestricted Grammars - Turing Machine

Context Free Grammar
-  좌변 : nonterminal 한 개
-  우변 : 제한 없음

Context Sensitive Grammar
-  좌변 : 제한 없음
-  우변 : 제한 없음
-  좌변의 길이가 우변의 길이보다 크면 안 됨
-  ε은 생성할 수 없음

Unrestricted Grammar
-  좌변 우변 형태 제한x 아무런 조건도x

Automata 종류
1. Finite-state automaton
-  각 상태에서 입력을 받으면 다음 상태로 전이되며, 마지막 입력을 받은 후에 종료 상태에 도달하면 입력을 수락

2. Pushdown automaton
-  PDA는 스택을 사용하여 입력을 처리하며, 각 상태에서 현재 입력 및 스택의 상단에 있는 기호를 기반으로 다음 상태 및 스택 조작

3. Linear-bounded automaton
-  튜링 머신과 유사하지만 테이프가 유한한 범위 내에 제한되는 모델
-  일반적으로 nondeterministic

4. Turing machine
-  R/W head
-  튜링 머신의 테이프는 무한한 길이를 가지며, 여러 개의 칸으로 구성되어 있다
-  각 칸엔 기호(Symbol)가 기록된다

@R/W head
-  테이프의 한 칸을 가리킨다
-  입력을 읽고, state와 transition function에 따라 이동 방향과 동작을 결정
-  결과를 테이프에 기록

@Decidability
-  Undecidable problem (튜링머신이 못 푸는 문제)
-  입력에 대해 언제 멈출 것인가 (halting problem)

Language Semantics
-  Static semantics를 나타내는 방법은 attribute grammar

Dynamic semantics
-  몇몇 입력에 대해 수행해 보면 됨?

Semantic Approaches
1. Grammatical Model
-  Attribute grammar
-  Grammar + evaluation rules
-  종합 속성 (노드의 속성 값이 자손 노드에 의존)
-  상속 속성 (노드의 속성 값이 부모 노드나 형제 노드에 의존)

2. Operational Model (Imperative Model)
-  Operational semantics
-  가상 기계상에서 프로그램의 동작
-  state, state transition mechanism

3. Applicative Model
-  Denotational semantics
-  프로그램의 의미를 함수로 파악
-  의미함수 (의미영역의 값을 다루는 함수)

4. Axiomatic Model
-  Axiomatic semantics
-  프로그램 수행 전과 후의 술어 변화가 프로그램 명세와 일치하는지 증명
-  Precondition, postcondition

5. Specification Model (Algebraic Data Types)
-  어떤 데이터에 대한 여러 함수의 관계를 정립
-  구현 내용이 이것과 동일함을 입증
-  Interface -> implement?

Axiomatic System (Program Verification)
-  Axiom
-  조건 없이 참

Axiomatic System
-  정리를 유도할 수 있는 임의의 공리 집합
-  Postcondition을 만족시키는 precondition을 찾는 것이 목표

The Weakest Precondition
-  주어진 사후조건에 대해 가장 제한이 덜한 사전조건
-  사후조건으로 부터 찾음
-  Input specification으로부터 유도 가능하면 correct
-  wp(A, Q)

Assignment Axiom
-  V := E
-  Value of V in final state is value of E in initial state
-  wp(V := E, Q) = Q[E/x]
-  Q[E/x] : Q에서 자유변수 x를 표현식 E로 치환한 것

@예시
{p} a := b/2 - 1 {a < 10}
wp(a := b/2 - 1, a < 10)
(a < 10)[(b/2 - 1) / a]
 b < 22

The Rules of Consequences
-  Weakening the postcondition
-  {P} S {Q}, Q := R // {P} S {R}
-  Strengthen the precondition
-  R := P, {P} S {Q} // {R} S {Q}
-  합치기 가능

The Rule of Composition
-  {P} S1 {Q}, {Q} S2 {R} // {P} S1; S2 {R}
-  wp(S1; S2, Q) = wp(S1, wp(S2, Q))

The Rule of Selection
{P ^ B} S1 {Q}, {P ^ ~B} S2 {Q} // {P} if B then S1 else S2 {Q}
wp(if B then S1 else S2, Q)
= (B => wp(S1, Q)) ^ (~B => wp(S2, Q))
= (B ^ wp(S1, Q)) ∨ (~B ^ wp(S2, Q))

The Rule of Iteration
-  Loop Invariant I
-  루프 내의 각 실행별 precondition을 모두 나타낼 수 있음
-  {I ^ B} S {I}
-  {I} while B do S {I ^ ~B}

@Loop Invariant For-Loop
1. for (init; test; step) S;

2. while로 변환
init;
while (test) {
  S;
  step
}

3. precondition, postcondition
{P}
[initialization step]
while (B)
S;
{Q}

4. loop invarant
{P} <- initialization precondition
[initilization step]
{I} <- initialization postcondition, loop precondition
while (B)
{I ^ B}
S;
{I}
{I ^ ~B} <- loop postcondition