형식증명용 언어이다.
실행 목적이 아닌 labare코드를 뱉는 용도이다.
output laber code의 구조 :
그러니까, 수학적인 Subrootine-Relationship 코드를 만드는게 목적이다.