CIS 771, Software Specification, Spring 2017

Reading Material: For the module involving Alloy, we'll use Software Abstractions by Daniel Jackson, published by MIT Press.
For other modules, relevant reading materials will be posted.


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:
Videos, slides and reading material for the course will be made available online. Students are expected to watch the video(s) and cover the slides and reading material on their own.
Lab sessions
Each Wednesday from 12:30-1:20pm, and each Monday from 12:30pm until around 1pm (longer or shorter as the demand may be), we'll meet in classroom 1061 in the Engineering building. This is an opportunity for you to ask questions (so make good use of it!) and for us to find out how your learning is proceeding. Attendance is strongly encouraged but not required.

Off-campus students will not have the benefit of participating in lab discussions, but they will receive copies of any exercises (with solutions) carried out during the lab.

Are given almost every week, usually Tuesday (due one minute before midnight) so they can be discussed at next day's lab session. They carry a total weight of 15% of the course grade.
There will be 4 homework assignments during the course, each counting 10% of the total grade.
Assignments that are late will be graded but, unless in case of exceptional circumstances (as defined later), with a penalty of 20 % per day.
There will be two midterm exams, on February 22nd and April 5th, in addition to the final exam on May 8th which is comprehensive but with emphasis on the last part of the course.
All exams are closed book (no material allowed), except for the final where one sheet will be allowed, and together count 45% of the total grade.

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.

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. (There may be an extra credit project, making it possible to score more than 100%.) 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.

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.

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; for K-State Polytechnic campus, contact Academic and Student Services at or call 785-826-2974.

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, 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.

Copyright as to 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