Course Outline

Course Code	SENG2011
Course Title	Workshop on Reasoning about Programs
Units of Credit	6
Course Website	https://webcms3.cse.unsw.edu.au/SENG2011/23T3/
Current hand-book entry	http://www.handbook.unsw.edu.au/undergraduate/courses/current/SENG2011.html

Course Summary

Reasoning involves taking what facts you know (or assume) to be true, and calculating what the consequences will be. Reasoning is what everyone does every day in real life: for example, *!#!* the traffic is bad this morning! I'm going to be late for work. My work says if employees arrive late, they must work overtime. I'll be working overtime tonight. This course applies reasoning to computer programming. It involves analysing the behaviour of the program using mathematical logic and creating a specification. This specification allows you to prove exactly what the program does. It means it is impossible for the program to contain any kind of programming error. This has important consequences for software development. It means, for example, a great deal less testing is required because you, the programmer, will be able to proudly promise that the program that you have produced is "perfect".

Course Aims

To learn the thinking, reasoning and programming skills required to write programs that are provably correct, and appreciate that this is the responsibility of every software engineer.

Student Learning Outcomes

If you successfully complete this course, you should have acquired a bunch of new skills:

• be able to build a formal specification of the behaviour of a program
• be able to write, or even engineer, code that conforms to the specification
• be able to reason abstractly about requirements and be able to model them using formal methods
• be able to implement the reasoning in the compiler/verifier language Dafny
• be aware that proving code is correct is necessary to achieve 100% system reliability

Assumed Knowledge

• essential is that you are competent in programming at least one procedural language (e.g. C, Python, Java)
  • e.g. can you write a program in your favourite procedural language that does linear search in an array?
• desirable is that you are familiar with logic and formal proof techniques
  • e.g. the propositional formula p→⌝q is equivalent to which of the following : [A] ⌝p→q [B] ⌝(p→q) [C] q→ ⌝ p [D] ⌝ q∨⌝ p ?
  • e.g. can you prove by induction that n! ≥ 2^(n−1) for n>0?
    
• desirable that you are familiar with Unix (e.g. Linux) commands, and interacting with the operating system

Answers to the above questions can be found here . Note that from the above you should be able to reason that being able to program is more important in this course than mathematical skills.

Teaching Strategy and Rationale

• The lectures form the backbone of the workshop. They act as a reference text (in slide form), but also as an over-arching tutorial that explains the concepts and processes by example.
  
  • Note: in surveys, many students recommend actually attending lectures (i.e. face-to-face)
• As SENG2011 is a workshop there are no tutorials: you are expected to make an extra individual effort.
• There is an active forum with a dedicated staff member.
• There will be multiple consultations with the course convenor, usually one consultation before and one after the lecture.
• On a regular basis there will be exercises to practice skills. These take the form of six weekly multiple-choice quizzes that test the concepts and two assignments that enable you to develop programming skills.
• Finally there is a programming examination at the end of the course. This examination should be (resources permitting) held in a closed laboratory: you will have no access to the course resources or even your own files.

The workshop is above all a 'practical' course, which means attaining competency in coding and verification is the primary aim.

Assessment

The total course mark will be the sum of the marks for the following components:

• Assessment 1: 6 weekly quizzes ( 10 marks total ) comprising multiple-choice questions (majority are multiple selection)
  • The final quiz mark will be calculate by the formula 10 * total-number-of-correct-answers / total-number-of-questions.
• Assessment 2: Assignment 1 ( 15 marks ) which is generally a mix of conceptual and programming exercises
• Assessment 3: Assignment 2 ( 25 marks ) comprising just programming exercises
• Assessment 4: Final Examination ( 50 marks ) comprising just programming exercises
  • There is a 'hurdle': if your final exam mark is below the final exam pass mark, your mark for the exam will be set to 0.
  • The pass mark for the final exam is scaled to the difficulty: the more difficult the exam, the lower the pass mark.
  • In individual cases, applying the hurdle always triggers a re-mark of the final exam.

Work will be marked against assessment criteria. Individual, on-line feedback will be provided for the assignments. There is on-line class-wide feedback for the quizzes, and verbal class-wide feedback during lectures for the assignments.

All the assessments should be done on an individual basis . A tentative schedule of when assessments are due can be found on the course website.

The late penalty is a per-day mark reduction equal to 5% of the max assessment mark, for up to 5 days, after which it will receive 0 marks. For example, if an assignment receives the mark 7/10 but was submitted 3 days late, its adjusted mark is 5.5/10.

If you think you have sound reasons to request a waiver of these rules, e.g. illness or misadventure, you must submit an official request for special consideration , with supporting documentation (e.g. medical certificates) through the formal UNSW central channels ( not by direct request to the convenor or system administrator.)

The supplementary exam :The course convenor has no control over who is eligible to take a supplementary exam. This is handled by Student Administration and requires you to apply for Special Consideration. If you are granted a Supplementary examination, then it will be held on a date specified by the university, or, if it is an on-line examination, it will be specified by the school. It is your responsibility to check at the School Office for details of Supplementary examinations.

Student Conduct

The Student Code of Conduct ( Information , Policy ) sets out what the University expects from students as members of the UNSW community. As well as the learning, teaching and research environment, the University aims to provide an environment that enables students to achieve their full potential and to provide an experience consistent with the University's values and guiding principles. A condition of enrolment is that students inform themselves of the University's rules and policies affecting them, and conduct themselves accordingly.

In particular, students have the responsibility to observe standards of equity and respect in dealing with every member of the University community. This applies to all activities on UNSW premises and all external activities related to study and research. This includes behaviour in person as well as behaviour on social media, for example Facebook groups set up for the purpose of discussing UNSW courses or course work. Behaviour that is considered in breach of the Student Code Policy as discriminatory, sexually inappropriate, bullying, harassing, invading another's privacy or causing any person to fear for their personal safety is serious misconduct and can lead to severe penalties, including suspension or exclusion from UNSW.

There is a document explaining the procedure for student misconduct.

If you have any concerns, you may raise them with your lecturer, or approach the School Ethics Officer , Grievance Officer , or one of the student representatives.

Plagiarism is defined as using the words or ideas of others and presenting them as your own . UNSW and CSE treat plagiarism as academic misconduct , which means that it carries penalties as severe as being excluded from further study at UNSW. There are on-line sources to help you understand what plagiarism is and how it is dealt with at UNSW: Academic Integrity and Plagiarism , and the Plagiarism Management Procedure .

• Make sure that you read and understand these documents.
• You are also responsible that your course assessment solutions are not accessible by anyone.
• Plagiarism includes paying or asking another person to do a piece of work for you and then submitting it as your own work.
  
• Posting exercises from the course assessments on the internet is considered an attempt to plagiarise, and accordingly such an action will result in penalties.

Resources for Students

The lecture notes are comprehensive, detailed and should be closely studied. Links to supporting documents such as the Reference Manual, excerpts from useful documents and published articles will also be provided on the website.

The book on this topic is Program Proofs by Rustan Leino has just this year (2023) been published and is available at amazon.com

Rustan Leino is an acknowledged leader in the field of formal methods of software engineering, and works at the cutting-edge of compiler development. The essential difference between this course and the book is that the course focusses on the language Dafny and how it is used to develop correct programs. The book is more conceptual and doesn't teach the language as such, but uses the language to demonstrate the concepts. The book is not referred to or used in any way in the course, but if you want to continue in the direction of formal verification, the book is a must.

References that explain the origins and form the theory of program verification are the following. These texts were written well before the language Dafny was created and are hence of limited use.

• Edsger W. Dijkstra : A discipline of programming
• David Gries : The science of programming
• Roland Backhouse: Program construction and verification
• Edsger Dijkstra and Wim Feijen : A method of programming

Course Evaluation and Development

137 students completed the 2022 workshop. The mark profile of the course is HD (14 students), DN (28), CR (28), PS (44) and FL (23). More concerning was 29 students commenced the course but withdrew during the term, did not submit the major assignment, or did not attend the final examination. The general feedback I received from these students was that they were unable to commit enough time to the workshop. Learning any language, natural or programming, requires practice, and some students need more practice than others to achieve a minimum level of language competency. While the language skills required to pass the workshop are similar to those you need to pass a first-year programming language course, the extra hurdle that you need to overcome is the logic, which plays a vital role. Get on top of that and you'll find the course straightforward and 'logical'.

The 'large' improvements in the workshop for 2023.

• The lecture notes have been completely revamped/re-styled. The organisation of material is now much clearer and cleaner.
• The first week's introduction to the mathematics of verification has been condensed and made more focussed.

The myExperience survey from 2022 revealed problems on several fronts:

• The quality of the lecture recordings was poor.
  • My fault as I didn't lecture with the recordings in mind so I was often off-screen. I'll do better in 2023.
• The workshop needs tutorials.
  • Tutorials are not scheduled for the workshop, but I might see what we can organise.
• It's hard to concentrate for the whole 3-hour lecture.
  • I often forgot to provide breaks in 2022. I'll be more disciplined this year and provide at least one decent break.
• The multiple-selection quizzes were too hard and due too soon after the lecture.
  • I need to find a better balance between easy and hard quiz questions. I'll work on that this year. BTW, if you look at the marks, this assessment was the hardest of all the assessments in 2022. Many students did much worse in the quizzes than in the final exam. A bad thing?
• The workshop needs more practice exercises and more Dafny resources.
  • There are few Dafny resources on the internet. Dafny is taught at many universities, but courses tend to make their material not-public. I've created a lot for this course and will continue to add more.
• The lectures slides were made accessible only after the lecture, and not before, which meant it was not possible to prepare for a lecture, or annotate slides during the lecture.
  • It just needs to be that way as I sometimes ask questions about the material on a slide, and show the answer on the following slide. I'll be increasing the use of this QA style in 2023. If I released the slides beforehand this would not work. As well, I alter the slides right up until the lecture and sometimes immediately afterwards if I find that slides can be improved.