This page in intended for Software Engineering students taking my SFWR ENG 2F03 course.

What's New?

• This Friday during my office hours I will give priority to SFWR ENG 2F03 questions from 14:30-15:30. From 15:30-16:30 SFWR ENG 4A03 questions get priority. Also Vera Pantelic, the graduate TA for the course will be in ITB/222 from 10:00-11:00 to answer questions on Friday.
• Detailed Assignment 4 Solutions are available in the Notes/Solutions subdirectory. Also for more examples of typechecking, induction, and software verification you can take a look at the 2001 Assignment 5 and its solutions.
• Previous years final exams are available for your study in the Notes/Examples subdirectory.
• Lecture notes on Higher Order Logic have been added and the lecture slides on modelchecking have been updated.
• Example solutions for the midterm are available in the Notes/Solutions subdirectory

The material covered in the course is taken from the following sources:

• Propositional Logic - Huth+Ryan Ch 1: 1.1, 1.4.1, 1.5.1, 1.5.2, 1.3, 1.2, then 1.4.2-1.4.3.
• Sequent Calculus and Proposition Logic in PVS - Course Notes
• Predicate Logic Semantics - Huth+Ryan Ch 2: 2.1, 2.2, 2.4.
• Predicate Logic Proofs - Huth+Ryan Ch 2: 2.3, 2.5
• PVS support for Predicate Logic - Course Notes
• Partial Functions in Logic - Course Notes
• Proof by Induction - Huth+Ryan Ch 1: 1.4.2 and Course Notes
• Higher Order Logic - Huth+Ryan Ch 2: 2.6 and Course Notes
• Software Verification - Course Notes and Dr. Baber's presentation (PDF)
• Model Checking - Course Notes and selected sections of Huth+Ryan

The detailed course outline is available in the following formats:

• HTML - including links to relevant slides
• pdf - including links to relevant slides

TA Support is available during your tutorial section's time.

Information on how to submit your PVS part of assignments is available here.

We will learn about two automated proof assistants (perhaps better described as "mechanized mathematics systems") in this course. They arePVS from SRI International and IMPS (originally developed by our own Dr. Bill Farmer and others at Mitre Corp.).

Lecture notes, examples (including old tests) are available in Postscript and PDF formats in the Notes Subdirectory.

For information on PVS, IMPS, Linux, X servers, printing the course notes and other interesting tidbits, checkout the 2F03 FAQ.

  
She says what she means
 And she means what she says.
When she says that I'm mean,
 Does she mean what she says?
 
from She says what she means on Sloan's Navy Blues.

Analysis of She says what she means:

S: Says what she means
M: Means what she says
I: Says that I'm mean

Q: Is S,M a valid argument for I -> M?

A: S,M |= I -> M iff S,M |- I -> M by completeness and consistency.
But S,M,I |- M      (Premise)
so  S,M |- I -> M   (Deduction Theorem) and therefore
    S,M |= I -> M   (Consistency)

NOTE: Do NOT use the link below to submit your assignments. It sends mail to my main account and is intended for comments on this page.