(C) Ralf Lämmel, Andrei Varanovich, University of Koblenz Landau
Logistics
- Course site
- Date published: 21 Nov 2012
- Deadline SVN: 27 Nov 2012 (End of Day)
- SVN: https://svn.uni-koblenz.de/softlang/main/courses/plt1213/students + group name
- Present your solution with your own system.
- Lab assistant calls up teams.
Assignment
Both assignments are carried out within Prolog.
1. An extension of NB
Consider the following Prolog-encoded semantics and typing rules of NB:
https://slps.svn.sourceforge.net/svnroot/slps/topics/semantics/nb
Modify the type system of NB by replacing the type Nat by Int (to represent integers instead of natural numbers). Also introduce the following types: Pos (to represent the subset of Int with positive numbers), Neg (negative numbers), and Zero ("0"). That it, Pos, Neg, and Zero can be considered subtypes of Int. With negative numbers enabled, you should also revise the semantics of pred to exercise negative numbers, actually. Demonstrate the type system with examples that exercise the more specific subtypes as well as the general type Int.
2. Semantics and type system of a language for stack-based operations
Consider the following operations:
- push i — pushes an integer literal i on the stack.
- push b — pushes a Boolean literal b on the stack.
- or — applies logical OR to top of stack and second top of stack, pops operands, pushes result.
- add — applies integer ADD to top of stack and second top of stack, pops operands, pushes result.
Describe the semantics for sequences of such operations as a mapping to the resulting stack of values.
Describe a type system for sequences of such operations as a mapping to the resulting stack of types of values.
Example 1
push True
push False
or
push 42
- Result of evaluation: [42, True]
- Result of type checking: [Int,Bool]
Example 2
push True
push False
add
- Result of evaluation: "your decision"
- Result of type checking: "not well typed"