22C/55:180 and basic understanding of logic and discrete structures (e.g., 22C:34)
The creation of new software is accomplished using a selected programming language, and the programming language provides a highly organized, precisely defined means for expression. This constitutes a rigorous basis for this ultimate step in software construction. However, the creation of any piece of software does not simply fall from one's fingertips. Substantial essential thinking must precede the act of generating the code itself. In the past, the phase of the intellectual process preceding the actual writing of code has not had a supporting formalism analogous to a programming language. Despite the fact that this phase of the process is more abstract (i.e., lacking specificity) and so in some ways more intellectually challenging, we have had to proceed informally with no real guide for our intuition. While intuition will never lose its place, "formal methods" is intended to provide the means for greater precision in both thinking and documenting this preliminary stage of the software creation process. When done well, this can aid all aspects of software creation: user requirement formulation, implementation, verification/testing, and the creation of documentation.
Our treatment of "formal methods" will be primarily concerned with the specification of software, and directly related issues. That is, developing a precise statement of what the software is to do, while avoiding explicit (or even implicit) constraints on how it is to be done. We seek to provide a fully rigorous description of the results a software item is to achieve while leaving the programmers with undiminished flexibility to use their ingenuity to attain those results. Since these descriptions of results are intended to precede the construction of the software and its execution by hardware, attaining precision and rigor necessitates the use of mathematical/logical formalisms. These platform independent specifications serve as an initial technical contract between the programmer and client, and subsequently guide the creation, verification, and documentation of the software. For additional perspective see
There will be an in-class (open book) mid-term on Monday March 6, and a (open book) final exam scheduled for 2:15 PM Monday May 8 in our regular classroom. There will also be regular homework assignments. The weighting of these items in grade determination is as follows:
|
homework |
30% |
|
mid-term exam |
25% |
|
final exam |
40% |
|
subjective |
5% |
You are encouraged to consult sources other than our texts (even if there is no directed reading assignment), including numerous pointers to on-line material that will be provided. You are also encouraged to discuss the course topics with your classmates since it is a genuinely helpful learning activity to formulate your own thoughts about the material sufficiently to express them to others (even general approaches to homework problems). But since the homework counts as a significant portion of your grade, it is expected that submitted work will be strictly your own; the department has explicit procedures for cheating that are described in the Graduate Handbook.