EECS 755

Software Requirements Modeling and Analysis


EECS 755 Blog

McClendon Office Hours

As many of you know, Brian McClendon has joined our faculty as a research professor. As developer of Google Earth and VP at both Google and Uber, Brian has great insight into both the technical and business side of computer science. Prof. McClendon is going to have general office hours if you want to come in and talk about a project or a career path. The first will be this Thursday 1pm-4:30pm. Sign up here.


Unfortunately, there are going to be lots of schedule changes at the end of the semester due to my trael. Important dates and changes are as follows:

If you miss everything else, do not miss the exam on 12/7!

Project 4

Project 4 is now available on Blackboard.

Midterm Scores

Assuming that I was able to successfully use blackboard, your miterm exam scores are available on the class blackboard site. The exam was great. I am quite happy with the class performance.


Someone in class today asked about closure of subtraction over nat in Coq. Actually, that wasn’t the question but it’s close enough for jazz. I commented that 0 - 1 = 0 in Coq to a number of well-deserved snickers. Turns out it’s true. To make subtraction closed over nat, subtraction results that would be negative are all 0. So it goes.


PolyList.v is another definition of list that is polymorphic over the type of the list contents. It is a rewrite of Natlist.v with the list type parameterized over content type. All proofs and definitions are re-done.

For your reading enjoyment I’ve also added some basic LTac definitions that take advantage of Coq’s proof scripting capability. LTac is a powerful language for writing tactics and reusing proofs. IN this example I use it to automate induction proofs. I also use autorewrite and rewrite databases to automate some mundane rewriting tasks.


As promised in class, I’ve created a yet another Coq project file Natlist.v that includes the natlist examples I did in class. Almost everything in the file is from Software Foundations, but I added a couple of things that Pierce does not talk about. One is the use of lemmas and the assert command and the other is a peek at using Ltac to simplify proofs. We will go over the rest of the module in class, but will likely not do much with Ltac right now. Just wanted to give you a taste of where we’re headed.


I’ve created a yet another Coq project file, Pairs.v, that includes the modules I presented in class yesterday. Another example of polymorphism very similar to the Stacks.v examples with the additional use of Notation.

Project 1 Available

Project 1 is now availabe in the projects section. It is a moderately more difficult problem set, but should still be reasonably easy. Some proofs require commands we have not learned as of September 14, but I wanted to let you get started now and experiment on your own.

Stacks and Polymorphism

I’ve created a Coq project file, Stacks.v, that includes the various stacks we’ve defined in class to illustrate poloymorphism in Coq. You will find several modules in the file each with a definition and several examples. There’s documentation in the file and I’ll add more when I have a chance. For now, load the file in Coq and play around.

There are no proofs at the moment, but you’ll discover the reason for that when you see your next project assignment…

Project 0 Available

Project 0 is now availabe in the projects section. It is a warm-up project intended to get you used to using the verifier. All proofs and definitions can be completed using techniques learned in class.