Syllabus

1 Prerequisites and Description

Prerequisite: a grade of C or better in CMSC330 or permission of instructor.

Credits: 3.

Description: Students will be introduced to a range of modern formal methods and software engineering practices, focusing on Dafny and Haskell. The first part of the course will look at Dafny, a verification-aware programming language that is used heavily at Amazon: students will learn different techniques for writing down precise specifications of desired system behavior and for proving that specifications hold of software artifacts. The second part of the course will focus on Haskell, with the goal of implementing a miniature version of Dafny split up in different exercises throughout the course of the semester. Knowledge of functional programming in the form of OCaml (from 330) is assumed, but not prior knowledge of Haskell or Dafny.

2 Course Workflow

The course will be based on live lectures and discussion. The main forms of communication will be ELMS (for main course announcements and grades) and Discord.

The discord server is there for you to organize as a class, ask questions of each other, and to get help from staff. That said, feel free to use the discord for discussion. I (Leo) will check periodically, but if you would like to ask a question directly to the course staff, office hours and email remain the prioritized forms of communication.

There is a channel ‘#course-discussion’ that is meant for discussion/questions/help regarding the material of the course, make sure that you keep that channel free from noise so that other students and course staff can easily see what issues are being brought up.

Discord invites will be sent out via ELMS announcement in the first week of classes. Ask the instructor or the TAs for invites if you haven’t received one. Make sure that your ‘nickname’ is set to something appropriate for class.

3 Office Hours

Office hours format will be announced closer to the start of the semster.

4 Topics

The following list of lecture topics will vary according to the pace of the course:

• Dafny
• Specifications with Dafny
• Hoare Triples/Verification Conditions
• Verification with Dafny
• From OCaml to Haskell
• Monads
• Parsing/Printing/State
• Property-Based Testing with QuickCheck
• Implementing (mini)Dafny

5 Grading

Grades will be maintained on ELMS.

You are responsible for all material discussed in lecture and posted on the class web page, including announcements, deadlines, policies, etc.

Your final course grade will be determined according to the following percentages:

6 Assignments

There will be several programming assignments, often with full week given for completion and submission (e.g. if it assigned on a Tuesday it will be due the following Tuesday at 11:59pm EST unless otherwise noted).

Up to two assignments throughout the semester will be accepted 2 days late no questions asked. Given the nature of the semester, additional accommodations can be granted — reach out to the instructor.

Assignments will be submitted through Gradescope.

7 Quizzes & surveys

There will be many quizzes and surveys. These will be administered through ELMS. Completed surveys receive full credit. Instructors reserve the right to reject survey responses that are not considered thoughtful.

8 Midterms

There will be one Midterm.

9 Project

There will be a course project that will be assessed during the final exam period for the course. It will constitute of putting together all of the (independent) semester assignments to get an end-to-end implementation of mini Dafny. The full project description will be distributed approximately a month before the due date.

10 Gradescope

Programming projects can be developed on your own system and subitted via Gradescope, which will provide virtual machines suitably configured for running your code. All project submissions must work correctly on the Gradescope VMs, and your projects will be graded solely based on their results on those machines. Because language and library versions may vary with the installation, in unfortunate circumstances a program might work perfectly on your system but not work at all on the VMs. Thus we strongly recommend that as you develop any project, you should run it several days early on Gradescope to have time to address any compatibility problems.

11 Outside-of-class communication with course staff

Course staff will interact with students outside of class in primarily two ways: office hours, and electronically via e-mail. The use of Discord and/or other classroom forums is allowed, and discussion amongst the students is encouraged, as long as the discuss is about the concepts and not the solutions. The majority of communication should be via office hours.

Personalized assistance, e.g., with assignments or exam preparation, will be provided during office hours. Office hours for the instructional staff will be posted on the course web page.

Additional assistance will provided via the ELMS class discussion forum. You may use this forum to ask general questions of interest to the class as a whole, e.g., administrative issues or problem set clarification questions. The course staff will monitor ELMS on a daily basis, but do not expect immediate answers to questions. Please do not post publicly any information that would violate the university academic integrity policy (e.g., problem set code).

ELMS allows students to send private questions that are only visible to instructors. Please use this feature if you wish to ask specific questions concerning your assignment solutions.

Personal e-mail to TAs should be reserved for issues that cannot be handled by the above methods.

Important announcements will be made in class or on the class web page, and via ELMS.

12 Excused Absences

Missing an exam for reasons such as illness, religious observance, participation in required university activities, or family or personal emergency (such as a serious automobile accident or close relative’s funeral) will be excused so long as the absence is requested in writing at least 2 days in advance and the student includes documentation that shows the absence qualifies as excused; a self-signed note is not sufficient as exams are Major Scheduled Grading Events. For this class, such events are the final project assessment and midterm, which will be due on the following dates:

• Midterm: TBD
• Final Project: TBD

For medical absences, you must furnish documentation from the health care professional who treated you. This documentation must verify dates of treatment and indicate the timeframe that the student was unable to meet academic responsibilities. In addition, it must contain the name and phone number of the medical service provider to be used if verification is needed. No diagnostic information will ever be requested. Note that simply being seen by a health care professional does not constitute an excused absence; it must be clear that you were unable to perform your academic duties.

It is the University’s policy to provide accommodations for students with religious observances conflicting with exams, but it is the your responsibility to inform the instructor in advance of intended religious observances. If you have a conflict with one of the planned exams, you must inform the instructor prior to the end of the first two weeks of the class.

For missed exams due to excused absences, the instructor will arrange a makeup exam. If you might miss an exam for any other reason other than those above, you must contact the instructor in advance to discuss the circumstances. We are not obligated to offer a substitute assignment or to provide a makeup exam unless the failure to perform was due to an excused absence.

The policies for excused absences do not apply to project assignments. Projects will be assigned with sufficient time to be completed by students who have a reasonable understanding of the necessary material and begin promptly. In cases of extremely serious documented illness of lengthy duration or other protracted, severe emergency situations, the instructor may consider extensions on project assignments, depending upon the specific circumstances.

Besides the policies in this syllabus, the University’s policies apply during the semester. Various policies that may be relevant appear in the Undergraduate Catalog.

If you experience difficulty during the semester keeping up with the academic demands of your courses, you may consider contacting the Learning Assistance Service in 2201 Shoemaker Building at (301) 314-7693. Their educational counselors can help with time management issues, reading, note-taking, and exam preparation skills.

13 Students with Disabilities

Students with disabilities who have been certified by Disability Support Services as needing any type of special accommodations should see the instructor as soon as possible during the schedule adjustment period (the first two weeks of class). Please provide DSS’s letter of accommodation to the instructor at that time.

All arrangements for exam accommodations as a result of disability must be made and arranged with the instructor at least three business days prior to the exam date; later requests (including retroactive ones) will be refused.

14 University of Maryland Policies for Undergraduate Students

Please read the university’s guide on Course Related Policies, which provides you with resources and information relevant to your participation in a UMD course.

15 Academic Integrity

The Campus Senate has adopted a policy asking students to include the following statement on each examination or assignment in every course: “I pledge on my honor that I have not given or received any unauthorized assistance on this examination (or assignment).” Consequently, you will be requested to include this pledge on each exam and assignment. Please also carefully read the Office of Information Technology’s policy regarding acceptable use of computer accounts.

Assignments and projects are to be completed individually, therefore cooperation with others or use of unauthorized materials on assignment or projects is a violation of the University’s Code of Academic Integrity. Both the person receiving assistance @bold{and the person providing assistance} are in violation of the honor code. Any evidence of this, or of unacceptable use of computer accounts, use of unauthorized materials or cooperation on exams or quizzes, or other possible violations of the Honor Code, will be submitted to the Student Honor Council, which could result in an XF for the course, suspension, or expulsion.

• For learning the course concepts, students are welcome to study together or to receive help from anyone else. You may discuss with others the assignment or project requirements, the features of the programming languages used, what was discussed in class and in the class web forum, and general syntax errors. Examples of questions that would be allowed are “Does a cond expression always end with an else-clause?” or “What does a ‘mismatched parenthesis’ error indicate?”, because they convey no information about the contents of an assignment.

• When it comes to actually writing an assignment, other than help from the instructional staff, assignments must solely and entirely be your own work. Working with another student or individual, or using anyone else’s work in any way except as noted in this paragraph, is a violation of the code of academic integrity and will be reported to the Honor Council. You may not discuss design of any part of an assignment with anyone except the instructor and teaching assistants. Examples of questions you may @bold{not} ask others might be “How did you implement this part of the assignment?” or “Please look at my code and help me find my stupid syntax error!”. You may not use any disallowed source of information in creating either the design or code. When writing assignment you are free to use ideas or short fragments of code from published textbooks or publicly available information, but the specific source must be cited in a comment in the relevant section of the program.

Violations of the Code of Academic Integrity may include, but are not limited to:

• Failing to do all or any of the work on a project by yourself, other than assistance from the instructional staff.

• Using any ideas or any part of another person’s project, or copying any other individual’s work in any way.

• Giving any parts or ideas from your project, including test data, to another student.

• Allowing any other students access to your program on any computer system.

• Posting solutions to your projects to publicly-accessible sites, e.g., on github.

• Transferring any part of an assignment or project to or from another student or individual by any means, electronic or otherwise.

If you have any question about a particular situation or source then consult with the instructors in advance. Should you have difficulty with a programming assignment you should see the instructional staff in office hours, and not solicit help from anyone else in violation of these rules.

It is the responsibility, under the honor policy, of anyone who suspects an incident of academic dishonesty has occurred to report it to their instructor, or directly to the Honor Council.

Every semester the department has discovered a number of students attempting to cheat on assignments, in violation of academic integrity requirements. Students’ academic careers have been significantly affected by a decision to cheat. Think about whether you want to join them before contemplating cheating, or before helping a friend to cheat.

You may not share, discuss, or compare assignment solutions even after they have been graded since later assignments may build upon earlier solutions.

16 Course Evaluations

If you have a suggestion for improving this class, don’t hesitate to tell the instructor or TAs during the semester. At the end of the semester, please don’t forget to provide your feedback using the campus-wide CourseEvalUM system. Your comments will help make this class better.

17 Right to Change Information

Although every effort has been made to be complete and accurate, unforeseen circumstances arising during the semester could require the adjustment of any material given here. Consequently, given due notice to students, the instructors reserve the right to change any information on this syllabus or in other course materials. Such changes will be announced and prominently displayed at the top of the syllabus.

18 Course Materials

Portions of the course materials are based on material developed by Stephanie Weirich.