Chapter4 Modeling Language Properties

Regular Grammar

• 형태
  • 좌변: nonterminal 한개
  • 우변: 정해진 한쪽 끝에만 nonterminal이 최대 한개 올 수 있음
    • 좌측 끝: left-linear grammar
    • 우측 끝: right-linear grammar
• 정규 문법의 예 
  • Id ->aX | ... |zX | a | ... |...| z (대문자는 nonterminal, 안올수도 있다)

Context Free Grammar

• 형태
  • 좌변: nontermial 한개
  • 우변: 제한 없음
• 문맥무관 문법 예
  • E -> E + T |T
  • T -> T*F|F

 

Context Sensitive Grammar

• 형태
  • 좌변의 길이가 우변의 길이보다 크면 안됨
  • 따라서 empty string (엡실론)은 생성할 수 없음
• 문맨민감 문법 예
  • S -> abc | aSBc
  • cB -> Bc
  • bB -> bb
  • L(G) = {a^n b^n c^n|n>=1}

Unrestricted Grammar (recursively enumerable grammar)

• 형태
  • 제한 없음
• 무제한 문법의 예
  • S -> ACab
  • Ca -> aaC
  • CB -> DB
  • CB ->F
  • L(G) = {a^n | n= 2^m, m>=1}

오토마타의 종류

 

튜링머신

• 읽고 쓸 수 있는 무한 길이의 테이프와 유한 제어로 구성된 유효 절차의 형식 모델
• 인간의 계산을 흉내 낸 기계
• memory: 무한 배열
• Control: read/ write 헤드, 좌우 이동

Church's Thesis

• 정리가 아니라 추론임
• Turing-Complete (Turing-Equivalent)
  • A가 turing-complete이라는 말은 A의 계산 능력이 튜링기계와 같다
  • 컴퓨터로 계산 가능하다는 의미로 받아들여 짐

Decidability

• Undecidable Problem
  • 튜링 머신으로 일반해를 찾을 수 없는 문제
  • 시간 제한 및 공간 제한 없음
• Halting Problem
  • Undecidable Problem의 대표적인 예
  • 주어진 튜링 머신과 입력에 대해 해당 튜링 머신이 멈출 것인가를 결정하는 문제 
  • 이 문제를 풀수 있나 못푸나를 결정하지 못함

Nondeterminism

 

Language Sementics

• 구문 표기의 기반
  • Regular Grammar ... 어휘 분석
  • Context-Free Grammar ... 구문 분석
  • CFG의 밖의 검사는 static semantics를 통해 검사
• 의미 표기
  • 이미 구문 분석은 끝났다고 가성
  • static Semantics를 나타내는 방법은 속성문법을 사용하는 것이 일반적임
  • 다이나믹 시맨틱스에 대해서는 여러 다양한 방법이 제안되고 있음

Dynamic Semantics의 어려움

• 프로그램의 수행 의미를 파악하는 방법?
  • 몇몇 입력에 대해 수행해 보는것 (테스팅)
  • 아직도 보편적으로 사용하는 방법
  • 그러나 모든케이스 확인이 아니다
• Defining Dynamic Semantics
  • 프로그램을 우리가 잘 아는 영역으로 끌여들여보자
  • 잘아는영역 예시
    • Abstract machine code -> Operational Semantics
    • Logical Predicates -> Axiomatic Semantics
    • Lambda Notations - Denotational Semantics

Semantic Approaches

• Grammatical Model
  • 속성문법: 문법의 각 기호에 속성을 부여하고 속성 값을 구하는 것으로 의미를 표현
• Operational Model (Imperative Model)
  • 기능적 의미론: 가상 기계 상에서 프로그램의 동작을 보임
• Applicative Model
  • 표기적 의미론: 각 프로그램이 나타내는 함수가 해당 프로그램의 의미라고 파악
• Axiomatic Model
  • 공리적 의미론: 프로그램 수행 전과 수행 후의 술어 변화가 프로그램명세와 일치하는지 증명
• Specification Model
  • 어떤 데이터에 대한 여러 함수의 관계를 정립하고, 구현내용이 이것과 동일함 을 입증

Attribute Grammars

• Attribute Grammars = Grammar + Evaluation Rules
  • 문법 기호에 속성을 부여
  • 속성을 구하는 규칙을 문법과 함께 제시
• 속성의 분류
  • 종합속성: 파스트리 노드의 속성 값이 자손 노드의 속성 값에 의존하고 있는 경우
  • 상속속성: 어떤 노드의 속성이 부모 노드의 속성이나 형제 노드의 속성에 의존하고 있는 경우

Operational Semantics

• 특징
  • 실제 컴퓨터와 유사한 가상기계의 동작을 통해 프로그램 의미를 표현
  • 가상기계
    • State: memory, registers, I/O devices에 대한 추상화
    • State Transition Mechanism: processor에 대한 추상화
• 상태변환 예

Denotational Semantics

• 특징
  • Applicative Model
  • 프로그램의 의미를 함수로 파악 -> 람다표기: 함수를 나타내는 데 유리함
  • 함수를 이용하여 프로그램을 설명함
• 의미함수
  • 의미영역의 값을 다루는 함수
  • 표기적 의미론은 구문에 해당하는 의미영역의 값을 반환하는 의미함수들로 구성됨
    • Binary: B -> N
    • Binary[[0]] =0
    • Binary[[1]] =1
    • Binary[[B0]] = 2* Binary[[B]]
    • Binary[[B1]] = 2* Binary[[B]] +1

 

Axiomatic Semantics

• 특징
  • 프로그램 요소에 대한 사전조건과 사후조건을 통해 프로그램의 의미를 파악
  • 프로그램 수행 측면 중 일부는 무시됨
• 사후조건 및 사후조건
  • {P} program {Q}
  • P:precondition- 프로그램 수행 전의 조건 (assertion)
  • Q:portcondition-프로그램 수행 후의 조건
  • 사전 조건은 input specification으로, 사후조건은 output specification으로 간주할 수 있다.

Algebraic Data Types

• 특징
  • 특정 타입 x와 관련된 함수들의 관계를 명시
  • 이러한 관계가 성립되도록 구현하였다면 해당 구현은 올바르다고 판단

 

Axiomatic System

• Axiom
  • 공리
  • 조건 없이 참이라고 전제된 어떤 명제
  • 가정과 결론의 형태를 갖는 공리를 특별히 룰이라고 하기도 함
• Axiomatic System
  • 정리를 유도할 수 있는 임의의 공리 집합
  • program이 precondition -> postcondition으로 가게 맞게 작성이 된건지 검증

 

The Weakest Precondition

• 주어진 사후조건에 대해 가장 제한이 덜 한 사전조건
• Weakest Precondition의 예
• {P} sum := 2*x + 1{sum>1}
  • P1: x>50
  • P2: x>10
  • ...
  • Px: x>0
  • Px쪽으로 갈수록 제약이 덜해진다. 범이가 가장 넓다.
• Weakest Precondition의 의미
  • 만약 weakest precondition이 프로그램 input spec.으로부터 추론된다면,
  • 또 사후조건이 원하는 output spec.이라면,
  • 프로그램은 원하는 일은 한다 ->Correct Program (요구사항대로 작동)

Assignment Axiom

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

The Rules of Consequences

• Weakening the Postcondition
  {P} S {Q}, Q=>R 를 만족하면 {P}S{R}
• Strenthen the Precondition
  R => P, {P} S {Q} 를 만족하면 {R} S {Q}
• 적용 예
  (x>5) => (x>3) , {x>3} x:=x-3{x>3}.   이면 {x>5}x:=x-3{x>0}

The Rule of Composition

• The Rule of Composition
  {P} S1 {Q} , {Q} S2 {R} 이면 {P} S1; S2 {R}
• 적용 예
  {P} y:=3*x +1; x:=y+3{x<10}
  Let Q = wp(y:=t+3,x<10)
  then P = wp(y:=3*x+1,Q)

The Rule of Selection

 

The Rule of Iteration

 

Impact of Program Verification

• Impact on the Language Design
  
  • 프로그램 증명을 어렵게 하는 기능은 언어에 포함되어서는 안된다. (예: aliasing)
  • assertion 첨가 기능: 프로그램 중간에 만족해야 할 조건
• Static Checkers
  • 프로그램이 만족해야 할 조건을 검사하는 프로그래밍 도구
  • 참고: Spec#, Boogie
• Modeling Language와의 결합
  • OCL = UML +constraints
  • JML 과 ESC/Java(Extended Static Checker for java)