McMaster University
Software Specification and Correctness
COMP SCI 3EA3 — Winter 2017
Instructor
Musa Al-hassy
ITB-229,
alhassm@mcmaster.ca
Teaching Assistant
Curtis D'Alves
ITB-229, dalvescb@mcmaster.ca
Office hours: In ITB-128 on Thursdays at 13:05-14:55.
Outline and Relevant Times
- Course Outline: available as
PDF
.
- Main textbook:
- Lectures: In BSB-105 on Mondays and Wednesdays at 8:30-9:30 and Fridays at 10:30-11:30.
- Tutorials: In BSB-B154 on Tuesdays at 14:30-15:30.
- Assessment: six bi-weekly quizzes, participation, and a final exam.
- Final Examination: Tuesday April 25, 2017 in University Hall 213 from 12:30pm to 3pm
( Here is a useful timetable generator for McMaster University students. )
News
Theorem List
Proving every non-axiom in a consistent (that is, non-cyclical) sequence is an excellent exercise!
- The exam will have lots of writing; best of luck!
The topics include
- Grammars and Induction
- Monoid/Lattice-based calculational proofs
- Searching algorithms
- ACSL specfications
- Quantifications
- Definitions, of course
Shin-Cheng Mu has an excellent set of slides for review:
Program Construction and Reasoning..
- Curtis will hold an exam review on Friday April 21 at 1-2:30pm in ITB-222.
- Due to the snowstorm cancelling tutorial, Quiz 5 is moved over to the next lecture.
- Binary Search will be on the upcoming quiz and on the exam.
- Updated the embedded DSL for C, alhassy_gcl2.h; it is now actually randomised.
- Fokkinga's A Gentle Introduction to Category Theory: the calculational approach
- The course text is in the bookstore!
- Sheet 2 posted early in-preparation for first quiz.
- The course text, an old version and the current version, are on reserve at Thode Library.
- First class on Wednesday, January 4.
Schedule — covered so far
Reports:
Pellets Puzzle with Frama-C |
; Importance of Algebraic Properties |
; (another report on) The Importance of Algebraic Properties |
; Comparing Variants of the Binary Search Algorithm |
; A Survey of Binary Search |
; A Comparison of Search Algorithms |
; Comparing and Contrasting Searching Algorithms and their Specifications |
; (another report on a) Survey of Binary Search |
; Theory to Practice: The Benefits of Correct-by-Construction Programming |
; (yet another report on) A Survey of Binary Search |
Scribed notes:
Lattices and Categories |
; Galois Connections
; The Mathematics of Programming |
; Weakest Preconditions |
; Fixed Points and Loops |
; Algorithm Derivation |
; Replacing Constants by Variables |
; Array Assignment |
; Bounded Linear Search |
; Finding an Invariant |
; Finding an Invariant |
; Heuristic Programming |
; Review and Goodbye |
Each week-date below has an accompanying PDF that contains
assigned readings, discussion of which is an integral part of class.
Moreover, such PDF's also contain suggested exercises that reinforce
the theory covered in class and serve as preparation for the quizzes,
and are covered in tutorial.
Possibly Interesting Literature and Links
- Further sources:
- “SoP”:
David Gries:
Science of Programming, Springer 1981,
ISBN-13: 978-1-4612-5983-1.
- “Cohen”:
Edward Cohen:
Programming in the 1990s, Springer 1990,
ISBN-13: 978-1-4613-9706-9.
- “Kaldewaij”:
Anne Kaldewaij:
Programming: The Derivation Algorithms, Pearson 1991,
ISBN-13: 978-0-1320-4108-9.
- “CbC”:
Derrick Kourie and Bruce Watson:
The Correctness-by-Construction Approach to Programming, Springer 2012,
ISBN-13: 978-3-642-27918-8.
— Freely accessible online to McMaster Students.
- “Van Gasteren”:
Netty Van Gasteren:
On the Shape of Mathematical Arguments, Springer 1990,
ISBN-13: 978-3-540-52849-4.
- “Using Z”:
Jim Woodcock and Jim Davies:
Using Z: Specification, Refinement, and Proof,
Prentice Hall 1996, out of print,
available on-line.
- “LADM”:
David Gries and Fred B. Schneider:
A Logical Approach to Discrete Math, Springer 1993,
ISBN-13: 978-0387941158.
(Related
website)
— This book was the CS 1FC3 / SE 2DM3 textbook 2010–2016.
-
“Huth-Ryan”:
Michael R. A. Huth and Mark D. Ryan
Logic in Computer Science, Modelling and Reasoning about Systems
Cambridge University Press, 2nd edition
2004, ISBN 0-521-54310-X
- Emacs:
“The extensible, customizable, self-documenting real-time display editor”
- Agda:
a dependently-typed functional programming language and proof assistant
Besides computational content, it permits verified proofs of our theorems; which,
due to Agda's mixfix unicode identifiers, is not significantly more effort than a conventional calculational presentation
in LaTeX. That is, Agda type checks our math.
- C
(Wikipedia),
a widely-used imperative programming language:
- Frama-C,
an extensible and collaborative platform dedicated to source-code analysis of C software.
- C99 (Wikipedia page)
is the version of C currently supported by Frama-C
Academic Ethics
You are expected to exhibit honesty and use ethical behaviour in all
aspects of the learning process.
Academic credentials you earn are rooted
in principles of honesty and academic integrity.
Academic dishonesty is to knowingly act or fail to act
in a way that results or could result in unearned academic credit or
advantage.
This behaviour can result in serious consequences, e.g. the grade of
zero on an assignment, loss of credit with a notation on the transcript
(notation reads: “Grade of F assigned for academic dishonesty”),
and/or suspension or expulsion from the university.
It is your responsibility to understand what constitutes academic
dishonesty.
For information on the various kinds of academic dishonesty
please refer to the Academic Integrity Policy, specifically Appendix 3,
located at
http://www.mcmaster.ca/academicintegrity
The following illustrates only three forms of academic dishonesty:
- Plagiarism, e.g. the submission of work that is not one's own or for
which other credit has been obtained.
- Improper collaboration in group work.
- Copying or using unauthorized aids in tests and examinations.
Discrimination
“The Faculty of Engineering is concerned with
ensuring an environment that is free of all adverse discrimination.
If there is a problem
that cannot be resolved by discussion among the persons concerned,
individuals are reminded that they should contact
the Department Chair,
the Sexual Harassment Office
or the Human Rights Consultant,
as soon as possible.”
Emergency Changes
The instructor and university reserve the right to modify elements of the
course during the term.
The university may change the dates and deadlines
for any or all courses in extreme circumstances.
If either type of modification becomes necessary,
reasonable notice and communication with the students will be given
with explanation and the opportunity to comment on changes.
It is the responsibility of the student to check their McMaster
email and course websites weekly during the term and to note any changes.