Problem Set 8

Due Date Formulating a solution to this problem set took me 300 lines of Redex code. Since this amount is about twice the maximal weekly load, I have decided to give you two weeks for this problem set. It is due on 18 March 2014.

Purpose This problem set asks you to formulate a type system for the model of a small class-based object-oriented programming language that you got to know for Problem Set 7. The PL research community has formulated the slogan "types prevent ‘message not understood’ errors" referring to the ideas that to call a method means to send a message.

Problem 1 Create at least five syntactically correct programs in CBOO that cause a run-time error in the current reduction semantics.

Do not use examples that declare two classes with the same name, a class with two identically named fields, a class with two identically named methods, or a method with two identically named parameters. While such problems may also trigger stuck states and should therefore be caught by your type system (in problem 2), they are not the kind of errors we are after.

Note: I have revised the model so that the unload function signals "run-time error" now when the reduction semantics gets stuck. The model also revises the syntax a bit to make programming in CBOO more like Java. See ** annotations.

Problem 2 Formulate a type system that prevents all run-time errors. Using classes as types is a questionable software engineering decision, but that it is not the point of this problem set. Start with the language of types, which currently provides only one single type. In this world, the language of types tends to include the names of (a program’s) classes. Hint Keep Object around as a type for the main expression; Object comes without fields and methods.

Next articulate judgment system. The main judgment, (typed p), holds if p type checks. The rules should type check suitably modified versions of the sample programs supplied with the model. They should not type check the programs from problem 1.

Hints (1) In essence, judgments are like functions and you must design them like functions. This means that to check the type correctness of a program, you will need a judgment for programs, classes, methods, and expressions. Each of the judgments will have one case per variant. (2) Most of this judgments must use accumulators, called contexts in type checking systems. For one of them it is best to keep the entire sequence of class declarations around, though if you’re up to it, you can strip out the information you need instead. (3) You will also need auxiliary judgments that retrieve the type of a class constructor from a class context; a field from a class context and a class name; and the type of a method from the same information.

Problem 3 Define the function typed-evaluate. It consumes grammatically correct programs from CBOO, type-checks them, and if they check out, runs them on the reduction semantics to produce a result. If the programs fail to type check, the function returns "type error".

Make sure that typed-evaluate returns "type error" for the sample programs from problem 1.

Deliverable Email a tar.gz bundle to my CCS email address whose name combines the last names of the pair in alphabetical order. The tar bundle must contain a single directory—with the same name as the tar ball—with a README.txt file and a 8.rkt Redex file.