McMaster University
Outline 
Jupyter Installation 

CAS 707 Specification Techniques
Emil Sekerinski
Term 2, 2022-2023

Outline

  • First class is on Wednesday, January 11. It is essential that everyone attends and introduces themselves.
  • This page is static. All announcements will be on Teams.

Location & Times

  • The classes are Wednesdays 3:00 pm - 4:20 pm and Fridays 10:30 am - 11:50 am. Classes are neither recorded nor streamed.
  • My office hour is after Wednesday's class. I am online on Teams generally Mondays, Tuesdays, and Thursdays in the afternoon.

Prerequisites

    Familiarity with programming is required. While CAS 701 Logic and Discrete Math is recommended, logic and discrete math with be reviewed over the course. Those who don't have sufficient background in logic and discrete math need to catch up on their own.

Course Objectives

    Programs are formal objects whose properties can be deduced with mathematical certainty solely from the program text, without execution. Conversely, programs can be designed to satisfy specifactions by construction in a way that can lead to leaner programs than first "guessing" the program. Complete specifications are meant to be easier to write, comprehend, and explain than programs implementing those. This course is on how abstraction in specifications is achieved and how adherence of programs to specifications can be verified. We focus on specifications of sequential and reactive programs. We consider both programs written in a simple algorithmic notation as well as programs in popular and special-purpose programming languages. Verification will be carried out by "paper and pencil" and by tools. Such tools have found industial use when reliability is of utmost importance, like in embedded systems and servers.

Required Reading

Course Notes
on jhub707.cas.mcmaster.ca
Dafny
Collection of Dafny Tutorials
Dafny Overview and Verification Condition Generation by Arie Gurfinkel
Event B
Jean-Raymond Abrial, Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010. The book is available online. See also the corresponding Slides and Rodin Platform Archives.
Rodin Handbook as pdf and html.
Rodin Tool and ProB Tool
Mini-course on Event-B and Rodin by Jean-Raymond Abrial.
More to be announced
...

Further Reading

Topics

  • Procedural abstraction (pre- and postconditions)
  • Weakest preconditions, verification, program derivation
  • Data abstraction (modelling), refinement
  • Specification of concurrency, exceptions, probabilities
  • Program algebra
  • Modelling, verification, and analysis tools (e.g. Dafny, ProB, Rodin)

Format and Attendance

  • The course has two overlapping parts: the first part consists of lectures and accompanying assignments.
  • The second part are individual projects with presentations on advanced topics. The topics will be assigned, but can be adjusted based on interest. Presentations will be 20 min in length and in style of conference presentations.
  • You are expected to attend all lectures and project presentations. If you miss one without explanation, you will be asked to withdraw from the course.

Evaluation

  • 4 Assignments, 10% each.
  • Project with presentation 50%; details will be announced.
  • Written project answers 10%; details will be announced.
  • If you MSAF any grade component, you get an extension.

Bibliographies

On-line Elements

    This course uses on-line elements (e-mail, Teams, JupyterHub). Students should be aware that, when they access the electronic components of a course using these elements, private information such as first and last names, user names for the McMaster e-mail accounts, and program affiliation may become apparent to all other students in the same course. The available information is dependent on the technology used. Continuation in a course that uses on-line elements will be deemed consent to this disclosure. If you have any questions or concerns about such disclosure please discuss this with the course instructor.

Academic Dishonesty

  • Assignments are to be completed individually; they must constitute your own work and references to all used resources must be given. Details are announced with each assignment.
  • Academic dishonesty consists of misrepresentation of deception or by other fraudulent means and can result in serious consequences, e.g. the grade of zero on all assignments, loss of credit with a notation on the transcript (notation reads: "Grade of F is 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. The following illustrates only three forms of academic dishonesty:
    • Submission of work that is fully or partly copied from someone else, or making your work available for copying to others.
    • Submission of work that has been fully or partly obtained from other sources like the Internet.
    • Copying or using unauthorized aids in tests and examinations.
  • All submitted assignments are always checked for similarities.

Conduct Expectations

  • As a McMaster graduate student, you have the right to experience, and the responsibility to demonstrate, respectful and dignified interactions within all of our living, learning and working communities. These expectations are described in the Code of Student Rights & Responsibilities (the “Code”). All students share the responsibility of maintaining a positive environment for the academic and personal growth of all McMaster community members, whether in person or online.
  • It is essential that students be mindful of their interactions online, as the Code remains in effect in virtual learning environments. The Code applies to any interactions that adversely affect, disrupt, or interfere with reasonable participation in University activities. Student disruptions or behaviours that interfere with university functions on online platforms (e.g. use of Avenue 2 Learn, WebEx or Zoom for delivery), will be taken very seriously and will be investigated. Outcomes may include restriction or removal of the involved students’ access to these platforms.

Academic Accomodation of Students with Disabilities

Academic Accomodation for Religious, Indigienous, or Spiritual Observances (RISO)

    Students requiring academic accommodation based on religious, indigenous or spiritual observances should follow the procedures set out in the RISO policy. Students should submit their request to their Faculty Office normally within 10 working days of the beginning of term in which they anticipate a need for accommodation or to the Registrar's Office prior to their examinations. Students should also contact their instructors as soon as possible to make alternative arrangements for classes, assignments, and tests.

Copyright and Recording

  • Students are advised that lectures, demonstrations, performances, and any other course material provided by an instructor include copyright protected works. The Copyright Act and copyright law protect every original literary, dramatic, musical and artistic work, including lectures by University instructors
  • The recording of lectures, tutorials, or other methods of instruction may occur during a course. Recording may be done by either the instructor for the purpose of authorized distribution, or by a student for the purpose of personal study. Students should be aware that their voice and/or image may be recorded by others during the class. Please speak with the instructor if this is a concern for you.

Extreme Circumstances

    The University reserves the right to change the dates and deadlines for any or all courses in extreme circumstances (e.g., severe weather, labour disruptions, etc.). Changes will be communicated through regular McMaster communication channels, such as McMaster Daily News, A2L and/or McMaster email.