Modeling Language Properties

촘스키 계층 (Chomsky Hierarchy)

• 형식 언어를 분류하는 4계층으로 나뉨. Type 0이 가장 복잡한 언어, Type 3가 가장 간단한 언어

Type 3 - 정규 문법 (Regular Grammar)

: 가장 간단한 언어. 아주 기본적인 패턴만을 표현할 수 있다

• FSA (Finite State Automata)로 인식 가능
• 예시: 0과 1로 구성됐는데, 1로 끝나는 문자열을 생성할 수 있다. transition의 끝이 1인지만 확인하면 되므로, 메모리가 없는 FSA만으로 인식 가능

Type 2 - 문맥 자유 문법 (Context-Free Grammar)

: 문맥을 신경쓰지 않는 간단한 규칙으로 만든 언어. 프로그래밍 언어의 문법을 정의할 때 많이 사용된다

• PDA (Pushdown Automata)로 인식 가능 (스택 == pushdown list)
• 예시: 괄호가 잘 닫혀 있는 문자열을 생성할 수 있다. 스택만으로 처리할 수 있으므로, 주변 문맥에 대한 정보가 없어도 PDA로 인식 가능

Type 1 - 문맥 민감 문법 (Context-sensitive Grammar)

: 문장에서 단어를 바꿀 때, 앞에 뭐가 있는지를 따지는 언어. 문맥에 따라 규칙이 달라진다

• LBA (Linear Bounded Automata)로 인식 가능
• 예시: a가 3개, b가 3개, c가 3개 있는 문자열을 생성할 수 있다.

Type 0 - 무제한 문법 (Unrestricted Grammar)

: 어떤 문자열이든 만들어 낼 수 있음. 문법 인식을 위해 튜링 머신 필요

Types of Automata

Finite-State Automaton

• 단방향 읽기만 가능

Pushdown Automaton

• 별도의 Pushdown List (Stack)을 가지고 있음

Linear-Bounded Automaton

• Read/Write Head를 가지고 있음

Turing Machine

• 읽고 쓸 수 있는 무한 길이의 테이프와 유한 제어로 구성된 형식 모델
• 인간의 계산을 흉내낸 기계

Church's Thesis

: 정리(Theorem)가 아니라 추론(Conjunction)이다!

• Any Computable Function can be computed by a Turing Machine
• 튜링 완전(Turing-Complete):
  • A가 튜링 완전하다는 말은, A의 계산 능력이 튜링 머신과 같다는 뜻
  • 컴퓨터로 계산이 가능하다는 의미로 받아들여짐

Decidability

• Undecidable Problem?
  • 튜링 머신으로 일반해(General Algorithm)를 찾을 수 없는 문제
  • 시간 제한 및 공간 제한은 없음(?)
• Halting Problem
  • Undecidable Problem의 대표적인 예
  • 주어진 튜링 머신과 입력에 대해, 해당 튜링 머신이 멈출 것인가를 결정하는 문제

Language Semantics

Grammatical Model

• 속성 문법(Attribute Grammar): 문법의 각 기호에 속성을 부여하고, 속성 값을 구하는 것으로 의미를 표현
  • Grammar + Evaluation Rules
  • 문법 기호(Grammar Symbol : terminal 또는 non-terminal)에 속성을 부여
  • 속성을 부여하는 규칙을 문법과 함께 제시

Operational Model

• 기능적 의미론(Operational Semantics): 가상 기계 상에서 프로그램의 동작을 보임
• 실제 컴퓨터와 유사한 가상기계의 동작을 통해 프로그램 의미를 표현
• 가상 기계?
  • State: memory, register, I/O device에 대한 추상화
  • State Transition Mechanism: processor에 대한 추상화

Applicative Model

• 표기적 의미론(Denotational Semantics): 각 프로그램이 나타내는 함수(Denotation)가 해당 프로그램의 의미라고 파악
• 의미 함수(Semantic Function)
  • 의미 영역(Semantic Domain)의 값을 다루는 함수
  • 표기적 의미론은 구문에 해당하는 의미영역의 값을 반환하는 의미함수들로 구성됨

Axiomatic Model

• 공리적 의미론(Axiomatic Semantics): 프로그램 수행 전과 수행 후의 술어 변화가 프로그램 명세와 일치하는지를 증명(Verification)
• 프로그램 요소에 대한 사전 조건(Precondition)과 사후 조건(Postcondition)을 통해 프로그램의 의미를 파악
  • {P} program {Q}
    • P: 프로그램 수행 전의 조건(Assertion)
    • Q: 프로그램 수행 후의 조건
    • 사전조건은 input specification으로, 사후조건은 output specification으로 간주할 수 있다!

Specification Model

• 어떤 데이터에 대한 여러 함수의 관계를 입증하고(Specification), 구현 내용이 이것과 동일함을 입증(Algebraic Data Type)

Axiomatic System for Program Verification

• 공리(Axiom):
  • 조건 없이 참이라고 전제된 어떤 명제
  • The assertions that are considered to be correct
  • 가정과 결론의 형태를 갖는 axiom을 특별히 rule이라 부르기도 함
• Axiomatic System
  • 정리를 유도할 수 있는 임의의 공리 집합
  • Any set of axioms from which some theorems may be derived

Weakest Precondition

• 주어진 사후조건에 대해, 가장 제약이 덜 한 사전조건
  • 만약 Weakest precondition이 프로그램의 input spec.으로부터 추론되고,
    프로그램의 사후조건이 원하는 output의 spec.이라면:
  • 올바른 프로그램이며, 프로그램이 의도대로 잘 동작한다는 의미!
• wp(P, Q) : 프로그램 P를 수행한 후, Q 조건을 만족하기 위한 weakest precondition
  • {wp(P, Q)} program {Q}

Assignment Axiom

{Q[E/x]} x := E {Q}

• 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/2-1) < 10
  • = b/2 < 11
  • = b < 22

The Rule of Consequence

• 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}

• 명제의 사후조건과 다른 명제의 사전조건이 겹칠 경우, 합칠 수 있다
• 적용 예시:
  • {P} y := 3 * x + 1 , x := y + 3 {x < 10}
  • 두번째 명제의 wp(x := y + 3, x < 10)를 Q라 하면
  • P = wp(y := 3 * x + 1, Q)

The Rule of Selection

{P ∧ B} S1 {Q}, {P ∧ ￢B} S2 {Q} 와 {P} if B then S1 else S2 {Q} 는 동등

• 적용 예시:
  • {P} if (x > 0) then y := y – 1 else y := y + 1 {y > 0}
  • wp(y := y – 1, y > 0) = y > 1
  • wp(y := y + 1, y > 0) = y > -1
  • (y > 1) ∧ (x > 0) ⇒ (y > 1)
  • (y > -1) ∧ (x ≤ 0) ⇒ (y > -1) ⇒ (y > 1)
  • 따라서, P = (y > 1)
  • (y > 1 ∧ x > 0) y = y – 1 (y > 0)
  • (y > 1 ∧ x ≤ 0) y = y + 1 (y > 2) ⇒ (y > 0)

The Rule of Iteration

{I ∧ B} S {I} 와 {I} while B do S {I ∧ ￢B} 는 동등

• 이때 I는 Loop Invariant!
  • 반복문 수행 전에 True
  • 반복문 수행 중에도 True
  • 반복문 수행 후에도 True
• 반복문의 WP를 찾기 위해서는 I(Loop Invariant)를 먼저 찾아야 한다
  • 어떻게? 추측 (Guess the Loop Invariant)
  • ...

• Program Verification 과정은 언어 설계에도 영향을 줌!!
  • aliasing처럼 프로그램의 증명을 어렵게 만드는 기능을 자제
  • assertion 기능의 필요성: 프로그램 중간에 만족해야 할 조건을 검사