SFWR ENG 2F03: Logic in Software Engineering

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

What's New?

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

The detailed course outline is available in the following formats:

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)
She does mean what she says when she says that I'm mean!

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.

Mark Lawford
Last modified: Thu Dec 9 11:56:58 EST 2004