McMaster University
Software Specification and Correctness
COMP SCI 3EA3 — Fall 2013
Instructor
-
Dr. Wolfram Kahl
ITB-245,
kahl at mcmaster dot ca
Office hour: Wed. 12:00-13:00, or by appointment (or catch me after class).
Teaching Assistant
- Yuhang Zhao —
zhaoy36 at mcmaster dot ca
Outline
The course outline is available as
PDF .
News
- Online communication in this course is normally handled via
Avenue.
Schedule
-
Lectures: Monday, Wednesday, and Thursday, 10:30-11:20, KTH-109
-
Tutorial: Tuesday 10:30-11:20, in T13-106 unless announced otherwise.
Tests
- Midterm Test 1: Monday, 21 October, 10:30–11:20, in T29-101
- Midterm Test 2: Thursday, 21 November, 10:30–11:20, in T29-101
Literature
- Main textbook:
- Further sources:
-
“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
- “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 is the CS 1FC3 textbook since 2010.
Links
- Logic Daemon
- Document preparation:
- LaTeX, the standard typesetting system for
Mathematics and Computer Science.
- Inkscape,
an SVG-based generic vector-drawing program
- Revision Control using Subversion:
- Computing environment:
- Programming Languages:
- Haskell,
a strongly-typed purely functional programming language
- Agda 2,
a dependently-typed functional programming language and proof assistant
- OCaml,
a strongly-typed functional programming language
with imperative and object-oriented features
- C
(Wikipedia),
a widely-used imperative programming language:
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 four 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.
- Collaboration where individual work is expected.
-
You have to produce your submissions for assignment questions
yourself,
and without collaboration
(except where and as far as group work is explicitly allowed or
specified by the assignment statement).
-
For each assignment question there will normally
be exercise questions similar to it ---
you are allowed to collaborate on these exercise questions.
(The tutorials are typically not expected to cover all exercise questions.)
- 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.