In this course we'll study Sun's Java Virtual Machine -- but in a very unusual way: we'll build a model of it in a functional programming language and we'll use an automatic theorem prover to reason about the model.
So you'll learn about three different things: how to model something complicated like the JVM, how to program in a simple functional language, and how to use a powerful automatic reasoning tool. Please come! (And yes, it is true, I bring homemade cookies to every class!)
Spring, 2007
We will study a formal specification of the Java Virtual Machine (JVM). The JVM is a stack-based, object-oriented, type-safe bytecode interpreter on which compiled Java programs are executed.
By ``formal specification'' we mean a collection of mathematical formulas that describe precisely the functionality of (part of) the machine. One of the main things you will learn in this class is how to characterize a complicated computing machine in terms of a mathematical logic.
A mathematical logic is a formal system consisting of a precisely defined syntax, some axioms, and some rules of inference. The axioms are just formulas in the syntax -- formulas that are taken to be ``always true.'' The rules of inference are formula transformers that preserve truth. A theorem is a formula that can be derived from the axioms by applying the rules of inference. A theorem is thus ``always true.'' By modeling a computing system in a mathematical logic we can prove theorems about it to establish its properties.
You studied formal mathematical logic in PHL313K and in CS336. There you learned propositional calculus as a formal system. You also learned first order predicate calculus. You might have also learned set theory. So which mathematical logic do we use to describe the Java Virtual Machine?
The mathematical logic we use is a functional programming language, Pure Lisp. If you know anything at all about Lisp, you probably think of it as merely a programming language. But we cast it as a logic, with a precisely given syntax, some axioms, and some rules of inference. We will prove theorems in Lisp.
Put another way, in this course you will come to understand the JVM by studying a model of the Java Virtual Machine written in a funtional programming language.
We will cover representatives of most of the JVM byte codes, including
IADD, ILOAD, ISTORE,
IFGT, GOTO, NEW,
PUTFIELD, INVOKEVIRTUAL, and
MONITORENTER. We will not cover the entire JVM -- for example,
we will not deal with the details of arithmetic, arrays, class loading, or
native methods. However, by the end of this course you will be able to write
formal specifications of many of the omitted parts.
We will discuss the Java bytecode verifier; in particular, we will investigate its specification: what properties should it have?
The logic we use is supported by a mechanical theorem prover, ACL2. This theorem prover is in use in industry to verify properties of hardware, microcode, and software. In fact, its authors won the 2005 ACM Software System Award for the lasting influence their theorem provers have had on computer science.
You will be using ACL2 extensively in this course. The homeworks will not be graded by a person. You will do them with ACL2 and evaluate for yourself whether you understand what we're doing in class. Some of the time you will be using ACL2 to prove theorems. More often you will be using it to define functions that formalize parts of the JVM.
This course is a cool mixture of many CS courses. It is like CS 307 in that we will be dealing with the Java programming language. It is like CS 310 in that we will be looking at an assembly level language. It is like CS 352 in that we will be considering the architectural features of the processor. It is like CS 372 in that we will be considering process management, memory management, protection, thread scheduling, and concurrency. It is like PHL 313K in that we will be dealing with a formal logic. It is like CS 336 in that we will be formally modeling and proving theorems about our programs and algorithms. It is like CS 343 in that we will be using a heuristic, rule-driven expert system to construct and check proofs mechanically.
My general plan for the semester is as follows.
javac,
and we'll think about how to prove properties of our code.
var, in
an environment, env, represented as a Lisp association alist.
(defun binding (var env)
(cond ((endp env) nil)
((equal var (car (car env))) (cdr (car env)))
(t (binding var (cdr env)))))
This function returns the value of var in env,
or nil if var is not bound in env.
This function is used in the formal model of the JVM, to specify what we
mean by ``the value of a variable in an environment.''
If you don't want to read stuff like this, don't take the course!
C
in an environment in which A has value 7,
B has value 5, etc.
(binding 'C '((A . 7)(B . 5) (C . -4) (D . 8)))The value of this expression is
-4. Lisp ``quote notation''
is used to represent byte coded programs, class declarations, etc.
(equal (car (cons x y)) x)This axiom tells us that the function
car, when applied to
the output of an application of cons, returns the first argument
of that application.
binding.
(equal (binding var1 (bind var2 val env))
(if (equal var1 var2)
val
(binding var1 env)))
This formula is a theorem of our Lisp logic. It expresses a truth
about binding. That truth is sloppily expressed by saying
``binding a variable only changes the value of that variable.'' If you don't
like precision, don't take the course! You will be expected to
prove some theorems in the course. In fact, you will be expected to prove them
by using the ACL2 theorem prover, which is an interactive, highly sophisticated
(and complicated) environment.
Previous exposure to Java and/or Lisp will be helpful but neither is necessary. The subset of Lisp we will use is quite small. The most disruptive idea you'll have to master is functional programming: programming without side-effects.
The development environment we'll use is an Eclipse interface to ACL2. Previous exposure to Eclipse will be helpful but, again, the environment we'll use is relatively simple.
You will learn to use the ACL2
system. ACL2 runs on the Department's public Linux machines. You may wish
to install ACL2 on your personal machine. See the Installation Instructions
on the ACL2 home
bpage. ACL2 runs under Windows, Linux and Macintosh. We'll explain in
class how to install the Eclipse interface.
Textbooks
Grades will be based on class participation and tests.
We will be using a version of ACL2 with an Eclipse front end. Early lectures will show you how to use it on public CS machines or install it on your own machine.
Assignments and solutions to exercises will be posted here.
Homework and Grading
The class meets Tuesdays and Thursdays. Almost every Thursday I will lecture and then post a new problem set related to that lecture. Solutions will be due before class the following Tuesday. Many solutions will take the form of a replayable ACL2 script to be run through the ACL2/Eclipse tool.
Suppose Problem Set 0 has only two problems. Problem 0.1 is to define a Lisp
function, incr, that takes two arguments and returns one more
than their sum. Problem 0.2 is to formalize the remark ``it doesn't matter
which order you write the arguments to incr'' by writing a
theorem and naming the theorem ``spec''. Here is an ideal
solution
; Problem 0.1
(defun incr (x y)
#|Are the arguments always supposed to be
numbers? We don't know. But we'll assume
they are numbers. We thought about adding
a test and doing something else if they
aren't numbers, but decided not to. Since
you don't generally read comments when
grading homeworks there is no point in our
saying this!|#
(+ 1 (+ x y)))
; Problem 0.2
(defthm spec
(equal (incr x y) (incr y x)))
Ask me or the TA if you are confused about a problem. When you send us email about homework problems, please use the subject line ``JVM homework''.
In the early part of the semester, the problems will be about ACL2 and how to define predicates and functions that express simple ideas and operations. Once we have introduced the operational semantics of bytecode, exercises will focus on expressing more complicated ideas. Some exercises will require you to prove theorems, by hand and with ACL2. Of necessity, the theorems will be very easy at the beginning and you will learn how to prove more complicated ones.
I strongly advise you to do all the homeworks!
Much of what we will learn will involve interpretation and formalization of vague English specifications. For example, consider the problem:
Problem 0.3
Is 0 an identity for the addition function? No.
(equal (+ 0 x) x) is not a theorem. Consider the
possibility that x is 'MONDAY. Fill in the blank
(***) to make the following a theorem:
(defthm left-identity-for-addition
(implies ***
(equal (+ 0 x) x)))
The ``perfect'' answer is to add the hypothesis that x is a number, expressed
in ACL2 by using the ACL2 predicate ``acl2-numberp'' as shown
below.
(defthm left-identity-for-addition
(implies (acl2-numberp x)
(equal (+ 0 x) x)))
If a student didn't know the name of the predicate for recognizing numbers and just guessed, writing something like
(defthm left-identity-for-addition
(implies (is-a-number x)
(equal (+ 0 x) x)))
then a grade of 0 would be assigned because the answer isn't syntactically
legal (there is no predicate named ``is-a-number'').
Could a technically correct answer receive a grade of 0? Yes! Here is an example.
(defthm left-identity-for-addition
(implies (equal (+ 0 x) x)
(equal (+ 0 x) x)))
This is technically correct in the sense that the student added a hypothesis
that makes the result a theorem. The student might also have added the
hypothesis (equal 1 2) or any other expression that is
identically false. Clearly, this answer is unacceptable.
You may say ``but if you don't want such answers you should have been more precise when you wrote the problem!'' My answer to that is simple: this course is about formal specifications and a key skill is figuring out what people mean when they speak or write ambiguous English.
(8) This note illustrates my grading guidelines on exams. Consider the sample problem:
Define (mem e x) so that it returns t if e is a
member of the list x and nil otherwise. Your
definition should make the following event
succeed.
(defthm mem-test
(and (mem 1 '(1 2 3))
(mem 2 '(1 2 3))
(mem 3 '(1 2 3))
(not (mem 4 '(1 2 3))))
:rule-classes nil)
A good solution would be:
(defun mem (e x)
(if (endp x)
nil
(if (equal e (car x))
t
(mem e (cdr x)))))
another might be
(defun mem (e x)
(and (not (endp x))
(or (equal e (car x))
(mem e (cdr x))))).
The following defun would receive a grade of 0 because it
contains a syntax error:
(defun (mem e x)
(if (endp x)
nil
(if (equal e (car x))
t
(mem e (cdr x)))))
even though the student's ``intention'' might be clear and correct.
The following defun would receive a grade of 0 because the ACL2
system rejects it for technical reasons.
(defun mem (e x)
(and (or (equal e (car x))
(mem e (cdr x)))
(not (endp x))))
(This may be disconcerting because the ``and'' expression above
is equivalent to the one in the acceptable defun of
mem. The technical problem is that the arguments to
``and'' are evaluated in left-to-right order and ACL2 does not
allow you to recurse on the cdr of x unless
x is known to be non-empty. As written above, the recursion
occurs before non-emptiness is tested. If this event is submitted to ACL2,
an error is printed. The error says that ACL2 cannot find an appropriate
``measure'' for this definition. The puzzled student should ask me or the TA
or some other student what's ``wrong.'')
The following ``solution'' makes the test formula a theorem but is not acceptable and would probably receive a grade of 0.
(defun mem (e x)
(if (equal x '(1 2 3))
(or (equal e 1)
(equal e 2)
(equal e 3))
nil))
This is a pretty lame solution because it doesn't satisfy the English
language spec even though it passes the announced test.
The reason I said it would ``probably'' receive a grade of 0 is that when the English specifications get more complicated legitimate misinterpretations are possible and if we notice that has happened we may give partial credit.