: program behavior(execution) 과 logic(predicate) 사이의 다리 역할
https://www.lazenca.net/pages/viewpage.action?pageId=6324534
predicate을 만든다. (symbol에 값을 넣었을 때 T/F값을 알 수 있는 것이 나오는 것)
-program analysis (pessimistic inaccuracy)
-Test data generation(optimistic inaccuracy)
-프로그램 correctness에 대한 Formal Verification(공식 검증)
critical 하위 시스템에 대한 철저한 검증
ex) safety kernel of a medical device
dynamic testing이 불가한 critical property 검증
ex) 보안
알고리즘 description(설명) 및 logical design 검증
→ 실행시키는 것 보다 덜 복잡하다.
Program Execution > Symbolic Execution하기
→ static analysis, model checking에서 assertion(precondition, roop invariant, post condition)을 제공 해줌
정보를 덜 가지고 있지만 correctness를 추론하는 데에는 충분하다.
Weakening the predicate 은 테스팅에 cost를 요구한다.
→ predicate을 만족하는 것은 program execution이 길 따라 잘 작동하는 데이터를 찾기에 충분하지 않다
⇒ W를 만족하는 test data는 path를 정상적으로 execute하긴 하지만, 충분하지 않음
⇒ W를 만족하지 않는 다는 것은 path가 infeasibility(실현가능하지않다) 라는 것을 보여줌
program이 static한 상태에서 판단하기 때문에(pessimistic) false alarm이 30%정도 존재한다. (correctness 판단 불가)
loop로 인한 execution path는 무한하다.
이를 추론하기 위해 loop를 Invariant(불변) 하게 만든다.
→ Assertion : 해당 지점에 도달할 때마다 true가 될 것이라고 예상되는 predicate 을 말함
invariant assertion에 도달할 때마다, weaken 할 수 있다.
: 사람이 제공한다.
: precondition이 주어지고, invariant한 loop를 다 실행한 후 postCondition을 만족한다면
⇒ pre&post condition에 대해 correct하다고 할 수 있다.
: precondition을 만족하고 block에 들어가서 postCondition을 만족하는 상태로 간다.
https://ropas.snu.ac.kr/~dreameye/PL/slide/PL10.pdf
Top을 증명한다면, 아래를 추론할 수 있다.
새로운 프로그래밍 언어를 만들었을 때 정상 동작을 증명하기 위해 위를 밝히면 아래를 추론할 수 있다.
: contract = precondition + postcondition을 만들어 놓고 필요한 곳에서 불러서 씀
Data Structure module
: Procedure(method) 의 모음 (specification이 강하게 연결된)
Contracts
: Procedure를 inner state의 abstract model(추상 모델)과 관련시킨다.
ex) Dictionary는 {<key,value>}로 abstract된다.
Dictionary는 독립적으로 list, tree, hash table 등에 사용된다.
Structural invariants
: maintain되어야 하는 structural 특징 (loop invariant와 비슷)
ex) tree class 내의 모든 method들은 key를 정렬해야 한다.
Abstract function
: concrete > abstract model states
