/Tiny-Semantics

Task for Semantics and Programs Verification course at MIMUW – denotational semantics of extended Tiny programming language in continuational style

Primary LanguageHaskell

Tiny-Semantics

Tiny is a minimalistic programming language featuring evaluation of simple expressions like +, -, * on integral numbers along with some basic logic expressions to handle if statements.

data Expr = LitInt Integer 
          | Var VarName
          | Plus Expr Expr
          | Minus Expr Expr
          | Mult Expr Expr

data BExpr = LitBool Bool
           | Con BExpr BExpr 
           | Eq Expr Expr 
           | Lt Expr Expr 
           | Neg BExpr

data Instr = Skip
           | Assign VarName Expr
           | Semicolon Instr Instr 
           | If BExpr Instr Instr 
           | While BExpr Instr 
           | Begin Decl Instr  -- new feature!
           | Call ProcName VarName  -- new feature!

This version of Tiny is extended with variable declarations and recursive procedures.

data Decl = VarDecl VarName Expr | ProcDecl ProcName VarName Instr | EmptyDecl | ConsDecl Decl Decl

All procedures take single argument by name reference and return nothing – the only way to gather it’s result is to assign new value to the argument, for instance evaluating program:

sample :: Instr
sample = Begin (ConsDecl
                (VarDecl "x" (LitInt 0))
                (ProcDecl "p" "y"
                 (Semicolon
                  (Assign "y" (LitInt 3))
                  (If (Eq (Var "x") (LitInt 3))
                   (Assign "y" (LitInt 4))
                   Skip
                 )
                )
               ))
         (Call "p" "x")

Will return state where x is bound to value 3.

The semantics of this language is written in continuational style as a task for MIMUW course.