CIS 771, Software Specification, Fall 2018

In the Fall 2018 semester, CIS771 is an online course, also for on-campus students;
there will be no classes or lab sessions.

Instructor: Torben Amtoft, tamtoft hat ksu dot edu, Engineering 2179.
Office Hours: Wednesdays 2-3pm, Thursdays 3-4pm, Fridays 1-2pm, and by appointment.


CIS 301, or familiarity with basic set theory.
We expect that you have had a software engineering course, and have some experience building some non-trivial programs in an object-oriented language.

Learning Outcomes:

The student should become familiar with technologies for software specification and verification that provide deep semantic reasoning about development artifacts such as functional models, architecture, and source-code implementations.

Topics: After a brief introduction, we shall cover

Course Organization:
Reading Material
Slides (and some supplementary reading material) are available on Canvas. (We expect you to study these on your own.)
For much of the material, video lectures are available (though some may be in an obsolete format)

For the module involving Alloy, we also suggest you read selected chapters from Software Abstractions by Daniel Jackson, published by MIT Press.

are given every Thursday (except when there is an exam); they are published at 3pm and are due one minute before midnight.
They carry a total weight of 18% of the course grade.

There will be 4 homework projects during the course (2 in Alloy, 1 in OCL/USE, and 1 in Logika), each counting 9% of the total grade.
Each project is due on Friday at 5pm (and will be posted at least two weeks earlier). Still, you can submit without penalty until Monday at 8am, but the instructor will not answer questions during the weekend.
Projects that are submitted later will be graded but, unless in case of exceptional circumstances (as defined later), subtracting 20 % of your score per day.

There will be two midterm exams (which for on-campus students are given on Thursdays between 9:30 and 10:45am); one is on Alloy and one is on OCL/USE, and each counts 14 % of the total grade. The midterm exams are closed book (no material allowed)

The final exam (which for on-campus students is given on Wednesday, December 12, 2:00-3:50pm) is comprehensive but with strong emphasis on Logika, and counts 18 % of the total grade. One sheeet of material will be allowed.

Distance students will need to arrange to have a proctor for the exams early in the term. You can arrange for this through K-state Global Campus, or contact the CS department office. Proctors are not needed for the weekly quizzes.

WeekExamProjectQuiz Slides studied
before quiz/exam
Aug 20-24#1 Course Overview
Sets and Relations
Aug 27-31#1 out#2 Alloy Tour (a,b,c)
Sep 4-7#3 Alloy Tour (d,e)
Sep 10-14#1 due#4 Alloy Logic (b,c)
Sep 17-21#2 out#5 Alloy Logic (d,e)
Sep 24-28Midterm 1
Oct 1-5#2 due#6 Introduction to OCL & USE
OCL Basics
Oct 8-12#3 out#7 More OCL
Oct 15-19#8 Advanced OCL
Oct 22-26#3 due#9 Invariants in OCL
Pre- and Post-conditions in OCL
Oct 29-Nov 2Midterm 2
Nov 5-9#4 out#10 Motivation
Nov 12-16#11 Methods
Nov 26-30#4 due#12 Termination
Dec 3-7#13 CaseStudies
Dec 10-14Final

Grading: Final letter grades are not based on strict percentage cutoffs but are "curved" by taking into account the difficulty of the exercises and exams. As a rule of thumb, however, you should expect that to earn an A it requires at least 85% total, and at least 75% for the exams, and to earn a B it requires at least 70% total, and at least 60% for the exams. In general, my approach to grading is expressed well by this piece by S.A. Miller.

An incomplete (I) final grade will be given only by prior arrangement in exceptional circumstances conforming to departmental policy in which the bulk of course work has been completed in passing fashion.

There will be NO make-up quizzes or exams. Special consideration will be given in only exceptional circumstances, in general limited to:

If you believe you qualify for exceptional treatment, you must notify the instructor prior to the date of the quiz or exam to be missed. Under exceptional circumstances, the missing quiz or exam will be ignored when computing the final score; otherwise, the student will get zero.

Computer Access While this course does not involve a lot of programming, it makes significant use of software tools. Many of these can be accessed by you (for free) and installed on your own machine.
If you prefer, we have everything you need on our CS department machines. See the computing systems page for information on how to get an account and use our machines.

Statement Regarding Academic Honesty
Kansas State University has an Honor and Integrity System based on personal integrity, which is presumed to be sufficient assurance that, in academic matters, one's work is performed honestly and without unauthorized assistance. Undergraduate and graduate students, by registration, acknowledge the jurisdiction of the Honor and Integrity System. The policies and procedures of the Honor and Integrity System apply to all full and part-time students enrolled in undergraduate and graduate courses on-campus, off-campus, and via distance learning. The Honor and Integrity System website can be reached via the following URL: A component vital to the Honor and Integrity System is the inclusion of the Honor Pledge which applies to all assignments, examinations, or other course work undertaken by students. The Honor Pledge is implied, whether or not it is stated: "On my honor, as a student, I have neither given nor received unauthorized aid on this academic work." A grade of XF can result from a breach of academic honesty. The F indicates failure in the course; the X indicates the reason is an Honor Pledge violation.

All your graded work must be completed independently. You are very welcome to discuss the course material, as well as specific questions, with your fellow students. However, all submitted answers must be your own work:

If you are in doubt about what is permissible, please ask me. If collaboration is discovered, students will be reported to the KSU Honor and Integrity program as violating the honors policy.

Statement Regarding Students with Disabilities
Students with disabilities who need classroom accommodations, access to technology, or information about emergency building/campus evacuation processes should contact the Student Access Center and/or their instructor. Services are available to students with a wide range of disabilities including, but not limited to, physical disabilities, medical conditions, learning disabilities, attention deficit disorder, depression, and anxiety. If you are a student enrolled in campus/online courses through the Manhattan or Olathe campuses, contact the Student Access Center at, 785-532-6441.

Statement Defining Expectations for Classroom Conduct
All student activities in the University, including this course, are governed by the Student Judicial Conduct Code as outlined in the Student Governing Association By Laws, Student Governing Association By Laws, Article V, Section 3, number 2. Students who engage in behavior that disrupts the learning environment may be asked to leave the class.

Acknowledgment: Most of the course material is adapted from previous courses taught by, among others, John Hatliff and Robby and Venkatash Ranganath.

Statement for Copyright Notification
Copyright 2018 (Torben Amtoft) as to this syllabus and all lectures. During this course students are prohibited from selling notes to or being paid for taking notes by any person or commercial firm without the express written permission of the professor teaching this course. In addition, students in this class are not authorized to provide class notes or other class-related materials to any other person or entity, other than sharing them directly with another student taking the class for purposes of studying, without prior written permission from the professor teaching this course.

Torben Amtoft