►CMSC631:   Program Analysis and Understanding
▼5 Problem sets
5.1 PS1
5.2 PS2
5.3 PS3
5.4 PS4
5.5 PS5
►5.2 PS2
On this page:
5.2.1 Problem 0
5.2.2 Problem 1
5.2.3 Problem 2
5.2.4 Problem 3
5.2.5 Problem 4
5.2.6 Delivery
6.2.0.5
    ← prev  up  next → 

5.2 PS2

Due: Midnight, Sept 30 (revised from Sept 23)

Purpose: The goal of this problem set is to improve your technical writing and to acquire basic competence in designing and implementing natural semantics, reduction semantics, and interpreters.

5.2.1 Problem 0

Revise the one-page description of your chosen programming language based on the feedback on PS1 handed back in class on September 11. Exchange memos with your partner. Critically mark up your partner’s memo to improve the writing. Together, revise both memos to incoporate the comments you generated. Commit PDFs of both revised memos to your github repository. (You may also commit source code, but I will only read the PDF.)

5.2.2 Problem 1

Implement an interpreter for the imprecise error semantics of the B language as a function in OCaml. Your interpreter is free to produce any answer that is consistent with the semantics.

This will require basic programming in OCaml. There are several tutorials to help get you started.

Suggestion: start by first solving the problem for B without variables, which will keep you from worrying about environments. After you have a working solution you can extend the interpreter to handle variables and environments. You will need to design a representation of environments and are free to use any design you are comfortable with. The simplest one is probably a finite list of pairs of variable names and values:

type env = (string * val) list

This definition assumes variable names are represented with strings and val is the type of values in your interpreter.

5.2.3 Problem 2

Develop a “maximally parallel” reduction semantics for the A language. The one-step reduction relation should apply as many occurrences of the reduction axioms as possible on every step.

Prove that the maximally parallel one-step reduction relation is a partial function.

Implement the function in OCaml.

Implement an interpreter in OCaml that iteratively applies the maximally parallel one-step reduction relation until a value is obtained.

5.2.4 Problem 3

Develop a standard reduction relation for the B language. The relation should be a partial function, i.e., a standard reduction step is deterministic.

Prove that for all B programs e, either e is an answer or e takes a step according to the standard reduction relation.

Implement the function in OCaml.

Implement an interpreter in OCaml that iteratively applies the standard reduction relation until an answer is obtained.

5.2.5 Problem 4

Develop a “potentially parallel" reduction semantics for the A language. The one-step reduction relation may apply any number of occurrences of the reduction axioms between 0 and the maximum.

Implement the reduction semantics in Redex.

5.2.6 Delivery

All work should be committed to your pair’s github repository. For proofs, you may submit PDFs, plain text files, or, if you’re so inclined, machine checkable proofs written in Coq, Agda, or other similar tools.

    ← prev  up  next → 
 

Web Accessibility