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 |
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".
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.
If you successfully complete this course, you should have acquired a bunch of new skills:
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.
The workshop is above all a 'practical' course, which means attaining competency in coding and verification is the primary aim.
The total course mark will be the sum of the marks for the following components:
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.
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 .
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.
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 myExperience survey from 2022 revealed problems on several fronts:
Resource created Friday 24 February 2023, 09:43:12 AM, last modified Saturday 13 May 2023, 12:15:56 PM.