CSE271: Principles of Programming Languages

Specification and Implementation

Jooyong Yi (UNIST)

Spec and Impl of Let Expressions

       (value-of 𝑒𝑥𝑝 ρ) = 𝑣𝑎𝑙                              [Spec]
---------------------------------------------
(value-of (let-exp 𝑣𝑎𝑟 𝑒𝑥𝑝 𝑏𝑜𝑑𝑦) ρ)
= (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟 = 𝑣𝑎𝑙]ρ) 

;; value-of : Exp * Env -> ExpVal                         [Impl]
(define value-of
  (lambda (exp env)
    (cases expression exp
      (const-exp (n)
        (num-val n)))    
      ...
      (let-exp (var exp body)
        (let ((val (value-of exp env)))
          (value-of body 
            (extend-env var val env))))))

zero?

[Concrete Syntax]
Program ::= Expression

Expression ::= ...
            |  zero? (Expression)

[Abstract Syntax]
Program ::= a-program (exp)

Expression ::= ...
            |  zero?-exp (exp)

Spec of zero?

       (value-of 𝑒𝑥𝑝 ρ) = 𝑣𝑎𝑙                              
---------------------------------------------
(value-of (zero?-exp 𝑒𝑥𝑝) ρ) 
= --- (bool-var #t) if (expval->num 𝑣𝑎𝑙) = 0
  |
  --- (bool-var #f) if (expval->num 𝑣𝑎𝑙) ≠ 0

Spec and Impl of zero?

       (value-of 𝑒𝑥𝑝 ρ) = 𝑣𝑎𝑙                              
---------------------------------------------
(value-of (zero?-exp 𝑒𝑥𝑝) ρ) 
= --- (bool-var #t) if (expval->num 𝑣𝑎𝑙) = 0
  |
  --- (bool-var #f) if (expval->num 𝑣𝑎𝑙) ≠ 0

;; value-of : Exp * Env -> ExpVal
(define value-of
  (lambda (exp env)
    (cases expression exp      
      ...
      (zero?-exp (exp)
        (let ((val (value-of exp env)))
          (let ((num (expval->num val)))
            (if (zero? num)
                (bool-val #t)
                (bool-val #f))))))))

Conditionals

[Concrete Syntax]
Program ::= Expression

Expression ::= ...
            |  if Expression then Expression else Expression

[Abstract Syntax]
Program ::= a-program (exp)

Expression ::= ...
            |  if-exp (exp1 exp2 exp3)

Spec of Conditionals

       (value-of 𝑒𝑥𝑝₁ ρ) = 𝑣𝑎𝑙₁
---------------------------------------------
(value-of (if-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂ 𝑒𝑥𝑝₃) ρ)
= --- (value-of 𝑒𝑥𝑝₂ ρ) if (expval->bool 𝑣𝑎𝑙₁) = #t
  |
  --- (value-of 𝑒𝑥𝑝₃ ρ) if (expval->bool 𝑣𝑎𝑙₁) = #f

Spec and Impl of Conditionals

       (value-of 𝑒𝑥𝑝₁ ρ) = 𝑣𝑎𝑙₁
---------------------------------------------
(value-of (if-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂ 𝑒𝑥𝑝₃) ρ)
= --- (value-of 𝑒𝑥𝑝₂ ρ) if (expval->bool 𝑣𝑎𝑙₁) = #t
  |
  --- (value-of 𝑒𝑥𝑝₃ ρ) if (expval->bool 𝑣𝑎𝑙₁) = #f

;; value-of : Exp * Env -> ExpVal
(define value-of
  (lambda (exp env)
    (cases expression exp      
      ...
      (if-exp (exp1 exp2 exp3)
        (let ((val1 (value-of exp1 env)))
          (if (expval->bool val1)
              (value-of exp2 env)
              (value-of exp3 env)))))))