This is the course homepage for Advanced Models and Programs (SASP), spring 2011.
Practical and administrative matters
7 June 2011: The exam will be held in room 2A20.
4 June 2011: Here is the exam schedule for Monday 20 June.
31 May 2011: All oral exams will be scheduled for Monday 20 June.
28 Feb 2011: The hand-in dates for Assignments 04 and 05 have been postponed by a week.
- Peter Sestoft (PS)
- Joe Kiniry (JK)
- Claus Brabrand (CB)
- Teaching assistants are David Christiansen, Dermot Cochran, Josu Martinez, Hannes Mehnert
- Project supervisors will include Dermot Cochran, Josu Martinez, Rolf-Helge Pfeiffer
Questions about the course contents and exercises can be posted at the course newsgroup it-c.courses.SASP at the news server news.itu.dk. Use Thunderbird to connect to the server and post to the newsgroup. Ignore postings from 2010.
The course starts on Monday 31 January 2011 at 1200.
The weekly course plan is as follows:
- Monday 1200-1400 in room 3A18 and 1400-1600 in room 2A54
- Wednesday 1200-1400 in room 2A18 and 1400-1600 in room 2A54
The course period is 16 weeks half time (15 ects). The course will consist of blocks, covering different themes, with weekly lectures and exercises; and a substantial six-week group project within one of the themes, resulting in a project report.
The weekly exercises must be handed in, and at least 8 of the 10 exercises must be approved to pass the course. You are allowed to work in groups to solve the exercises, but each individual student must write his/her solution up individually and hand it in by him/herself.
Here is the SASP2011 List of Approved Weekly Exercises.
More precise hand-in rules for weeks 1-5:
- Ensure that the zip file unpacks to a directory with the same name as the file. For example, SASP-02-DavidChristiansen.zip should contain a top-level directory SASP-02-DavidChristiansen/ that then contains the files being submitted.
- Add comments immediately next to all code relevant to a particular exercise that contains the exercise number. For example:
// 1.1 Time t1 = new Time(5, 35); Console.WriteLine(t1);
The project must be done in groups (2-4 people in each group) and the project report must be presented in an oral exam, where questions may be asked in all themes of the course.
As stated above, and in keeping with the course learning outcomes, the project must be documented by a project report. Here is some advice on report writing.
For an explanation of how to hand in the final project, see the ITU Intranet.
Here is the SASP2011 List of Project Submissions.
The official course description says:
"The project report must be presented in an oral exam, where questions may be asked in all themes of the course. A single grade is given, based on the project and the oral exam."
"Ekstern censur, [7-trinsskala], B4: Mundtlig eksamen med skriftlige arbejder men uden forberedelsestid ved eksamen."
We allow a total of 15 minutes for project presentation (by the whole group) and feedback followed by 15 minutes of individual examinations of each student. The individual examinations will cover both the project and all other aspects of the course. The official explanation, found at the ITU intranet, says (in Danish):
"Projekter udarbejdet i gruppe afsluttes med en fælles præsentation umiddelbart før afholdelse af eksamen. Denne præstation er ikke en del af eksamen. I skal være opmærksom på at ved den efterfølgende eksamination eksamineres alle gruppemedlemmer i hele gruppeopgaven.
Hvis en mundtlig eksamen tager udgangspunkt i en rapport eller et skriftligt arbejde, som er udarbejdet af flere studerende, må hvert gruppemedlem først være til stede i eksamenslokalet, når gruppemedlemmet selv skal eksamineres."
The oral exam will take place Monday 20 June in room 2A20 [and no longer on Tuesday], according to this exam schedule.
Intended Learning Outcomes
The course has two parts as detailed under course form below - a regular course followed by a project.
After the course, the students are expected to be able to:
- describe relevant concepts within the themes of the course,
- account for the practical applications of the covered constructs, and
- compare selected techniques and constructions within a single of the course themes.
On the basis of the project, the student are expected to be able to:
- apply relevant methods and techniques in the chosen project
- argue for the overall design-decisions in the project, and
- relate project and theory.
See also the Official Course Description.
The themes covered in the course include
- Programming language concepts
- C# and how it differs from Java
- Lexing, parsing and compilation: From source code to abstract syntax to stack machine code
- Functional programming in C#, Scala and Scheme
- Program generation, quasi quotations, program specialization
- Applied formal methods in practice
- Program specification and verification with BON, JML, and Java
- Static analysis; in particular, data-flow analysis
The rightmost column shows, for each week, the number of hours (scheduled teaching + preparation + mandatory exercise/report work) that we expect a student to work with this course. Please tell us if those numbers are way off relative to the work you feel you need to put in.
|05||Mon 31 Jan||PS||C# vs Java: non-virtual methods, properties, indexers, operator overloading, value types, enum types, reference parameters.|| Slides PS1 and
C# Precisely second edition sections 5.2, 7.2, 9, 10.7-8, 10.15-10.18, 12.17.2, 12.18-19, 13.6, 13.10, 14, 16, 17, 29
|Assignment 1||8+8+7 h|
|Wed 2 Feb||PS||C# vs Java: iterator blocks, generic types and methods, anonymous methods, C# 3.0: inferred types, extension methods, ...|| Slides PS2 and Slides PS3
and C# Precisely second edition sections 6, 10.9, 12.10-11, 12.22-25, 13.12, 19, 26, 28
|06||Mon 7 Feb||PS|| C# 3.0 and 4.0: anonymous objects, object and collection initializers, Linq; default parameters, named arguments, variance in type parameters, the type dynamic;
(maybe) asynchronous programming
| Slides PS3
and C# Precisely second edition sections 6.4, 10.10, 18, 22, 23, 26.12
|Assignment 2||8+8+7 h|
|Wed 9 Feb||PS||Scala: object-oriented and functional programming combined, traits, ...||Slides PS4 and Scala Tutorial and An Overview of the Scala Programming Language|
|07||Mon 14 Feb||PS||Abstract syntax, interpretation and checking; lexing and parsing ...||Slides PS5 and Mogensen sections 2.1-2.9 and 3.1-3.6. Sestoft PLCSD chapters 1-3.||Assignment 3||8+8+7 h|
|Wed 16 Feb||PS||Grammar transformations, compilation and stack machines ...||Slides PS6 and Coco/R User Manual pages 1-17, 23-28. Sestoft PLCSD chapters 1-3 and 8.2|
|08||Mon 21 Feb||PS||Micro-C and pointers.||Slides PS7 and Kernighan and Ritchie 1988 pages 93-110 and Sestoft PLCSD chapters 7-8||Assignment 4, hand-in postponed to 11 March||8+8+7 h|
|Wed 23 Feb||PS||Bytecode, abstract machines, and real machines.||Slides PS8 and Sestoft PLCSD chapters 9-10. Sestoft: Numeric performance in C, C# and Java and Ecma-335 CLI standard, partition I, section 12.3|
|09||Mon 28 Feb||PS||Just-in-time compilation and performance. Start on program generation and Scheme.||Slides PS8 and Slides PS9||8+8+7 h|
|Wed 2 Mar||PS||Scheme, multi-stage programs, partial evaluation||Slides PS9 and Dybvig sections 2.1-2.7, 6.1||Assignment 5, hand-in postponed to 18 March|
|10||Mon 7 Mar||PS|| Runtime code generation (1.5 hours) and some words about projects.
Student presentation by Bastian Müller: The Lua JIT compiler (0.5 hour).
|Slides PS10 and Sestoft PLCSD chapter 14||8+8+7 h|
|Wed 9 Mar||JK||Background, Business Object Notation, and Analysis (Example Projects, Effective Use of Formal Methods, The Business Object Notation, Dependable Systems Analysis)|| Slides JK1 |
Screencast on OpenJDK and Eclipse
| Assignment 6,
hand-in 21 March
|11||Mon 14 Mar||JK||Emergency guest lecture by Dermot and Josu.||Completing lecture on Informal BON and small-group exercise on analysis||8+8+7 h|
|Wed 16 Mar||JK|| Specifications (Assertions and Specifications,
Contracts and Specifications in BON and JML)
| Slides JK2 |
Scenarios and Events Screencast
| Assignment 7,
hand-in Monday, 28 March
|12||Mon 21 Mar||JK||JML (Introduction to JML, Applying BON to Java and JML)|| LeavensBakerRuby99, LeavensEtAl00, LeavensCheon06, LeavensEtAl05||8+8+7 h|
|Wed 23 Mar||JK||Static Analysis (Code Standards and Metrics, Static Analysis for Software Construction)|| Slides JK4 |
|13||Mon 28 Mar||JK||Validation (Testing, Types of Testing, Unit Testing, Testing in Practice, Testing with Specifications)|| Slides JK5 |
| Assignment 8,
hand-in Monday, 4 April
|Wed 30 Mar||JK||Verification (Kinds of Verification, Details of a Verification Tool, Model Checking, Using Verification Effectively)|| Slides JK5 |
Example Validation Workspace
| Assignment 9,
hand-in Monday, 11 April
|14||Mon 4 Apr||CB||Undecidability, Static Analysis, Data-Flow Analysis, and Control-Flow Graphs.||Slides CB1 Lecture Notes (Chapters 1, 2, and 5; i.e., pages 3-6 + 15-17).||Assignment 10 hand-in Wednesday, 27 April||8+8+7 h|
|Wed 6 Apr||CB||(Project presentation 12:00-12:20). "Extraterrestrial Mathematics" (which we need for Data-Flow Analysis).||Slides CB2 How to solve recursive equations|
|15||Mon 11 Apr||CB||Data-flow Analyses in practice; we'll study examples.||Slides CB3||8+8+7 h|
|Wed 13 Apr||CB||Data-flow Analysis Workshop|
|16||Mon 18 Apr||Easter break||0+0+0 h|
|Wed 20 Apr||Easter break|
|17||Mon 25 Apr||Easter break||0+0+24 h|
|Wed 27 Apr||Projects|
|18||Mon 2 May||Projects||0+0+24 h|
|Wed 4 May||Projects|
|19||Mon 9 May||Projects||0+0+24 h|
|Wed 11 May||Projects|
|20||Mon 16 May||Projects||0+0+37 h|
|Wed 18 May||Projects|
|21||Mon 23 May||Projects||0+0+11 h|
|Wed 25 May||Project reports must be handed in no later than 1500 on Wednesday 25 May|
Literature and materials
On C# 3.0 and 4.0 and Scala
- As reference material on C#, you'll get a copy of the draft manuscript for Sestoft and Hansen: C# Precisely, second edition (MIT Press 2011). See the book's home page and examples.
- To compile and run C# programs, you can use Visual C# Express 2010 or Mono (especially for Linux and MacOSX)
- To compile and run Scala programs, Download and install Scala (you'll need a java runtime).
- To learn Scala, start with a Scala tutorial.
- Then read An Overview of the Scala Programming Language, which is a short but rather dense walkthrough of the features of Scala. But note that the paper is from 2006 and the syntax used in some examples is now outdated.
- Scala library documentation online
- Overview of the Scala collection classes
On compilation and abstract machines
- Torben Mogensen: Basics of compiler design
- Coco/R lexer and parser generator, User Manual pages 1-17, 23-28
- Peter Sestoft PLCSD: Programming Language Concepts for Software Developers, version 0.50, September 2010, PDF.
- Here is a zip-file of all zip-files of example files for Programming Language Concepts.
- Expressions.ATG, lexer and parser specification for simple expressions
- Expressions.cs, interpreter, checker, compiler for simple expressions
- Machine.cs, stack machine to evaluate compiled expressions and execute compiled micro-C programs
- ex1.txt, a tiny "program" in the expression language
- A Makefile for Assignment 3 with Mono and Linux, thanks to Martin Kjeldsen.
- Kernighan & Ritchie: The C Programming Language, 1988, pages 93-110. (About pointers and pointer arithmetics). This will be handed out in paper form.
- MicroC.ATG, lexer and parser specification for micro-C
- MicroC.cs, interpreter, checker and compiler for micro-C
- test-c.zip, a bunch of micro-C test programs and an input file a.in
- Selsort.cs and Selsort.java, programs for Assignment 4
- GenericExample.cs and GenericExample.java, programs for Assignment 4
- Ecma-335 Common Language Infrastructure specification, the standardization of Microsoft CLR and Microsoft Intermediate Language, 2010; the PDF file contains a detailed description of the .NET bytecode instructions
- Jeffrey Richter: CLR via C#, Microsoft Press 2006, pages 3-22.
- Lindholm and Yellin: The Java Virtual Machine specification, Addison-Wesley 1999
- Peter Sestoft: Numeric performance in C, C# and Java, ITU 2010.
- The Intel x86 machine code is described in two documents: Intel® 64 and IA-32 Architectures Software Developer's Manual Volume 2A: Instruction Set Reference, A-M and Volume 2B: Instruction Set Reference, N-Z. Warning: This is 1650 pages in total.
- A more compact description of x86 instructions is found in appendix B of the manual for the open source x86 assembler "nasm"
- Example assembly language programs (x86, Linux, Windows, MacOS): nasm-examples.zip
- x86-64 Machine-Level Programming notes by Bryant and O'Hallaron, CMU.
- The Racket Scheme system, available for multiple platforms. First time you use it, configure: Language > Choose language > Legacy Languages > Pretty Big. To time evaluation of expression e, evaluate (time e).
- The SCM system by Aubrey Jaffer. Neat and simple system, especially for Linux; slightly more complicated to install under Windows.
- R Kent Dybvig: The Scheme Programming Language, MIT Press 2003
- Jones, Gomard, Sestoft: Partial Evaluation and Automatic Program Generation, Prentice-Hall 1993.
- RTCG2D2.cs, an example of runtime bytecode generation in .NET
On the Business Object Notation
- [BonMethodWebsite] The BON Method website (http://www.bon-method.com/)
- [Walden98] Kim Waldén, Business Object Notation (BON). Chapter 10 of the Handbook of Object Technology, CRC Press, 1998.
- [PaigeOstroffFM99] Richard Paige and Jonathan Ostroff, Developing BON as an Industrial-Strength Formal Method. LNCS 1708, Proceedings of Formal Methods '99, 1999.
- [WaldenNerson94] Kim Waldén and Jean-Marc Nerson, Seamless Object-Oriented Software Architecture: Analysis and Design of Reliable Systems. Prentice-Hall, 1994.
- [PaigeOstroffUML99] Richard Paige and Jonathan Ostroff, A Comparison of the Business Object Notation and the Unified Modeling Language. LNCS 1723, Proceedings of UML'99---The Unified Modeling Language, 1999.
On the Java Modeling Language (JML) and System Validation and Verification
- [BurdyEtal02] Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary Leavens, K. Rustan M. Leino, and Erik Poll, An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 2005. (Available via SpringerLink in ITU's digital library.)
- [LeavensEtAl00] Gary Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. Technical report #00-15, Iowa State University, 2000.
- [LeavensCheon06] Gary Leavens and Yoonsik Cheon. Design by Contract with JML.
- [LeavensEtAl05] Gary Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming, vol. 55, issues 1-3, March 2005.
- [CokKiniry05] David Cok and Joe Kiniry. ESC/Java2: Uniting ESC/Java and JML. LNCS 3362, Proceedings of CASSIS'04, 2005.
- [LeavensBakerRuby99] Gary Leavens, Albert Baker, and Clyde Ruby. JML: A Notation for Detailed Design. Chapter 12 of Behavioral Specifications for Businesses and Systems, Kluwer Academic Publishers, 1999.
- [CheonLeavens02] Yoonsik Cheon and Gary Leavens. A simple and practical approach to unit testing: The JML and JUnit way. LNCS 2374, Proceedings of ECOOP'02, 2002.
- [KiniryCok04] Joseph Kiniry and David Cok. "ESC/Java2: Uniting ESC/Java and JML". Proceedings of CASSIS 2004.
- [ChalinEtAl05] Patrice Chalin, Joseph Kiniry, Gary T. Leavens, and Erik Poll. "Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2". The 4th International Symposium on Formal Methods for Components and Objects (FMCO 2005). Amsterdam, The Netherlands. November, 2006.
- [JanotaGrigoreMoskal07] Mikoláš Janota, Radu Grigore, and Michał Moskal. "Reachability Analysis for Annotated Code". The 6th International Workshop on the Specification and Verification of Component-based Systems (SAVCBS 2007). Dubrovnik, Croatia. September, 2007.
- [KiniryZimmerman08] Joseph Kiniry and Daniel Zimmerman. "Secret Ninja Formal Methods". The 15th International Symposium on Formal Methods (FM 2008). Turku, Finland. May, 2008.
- [KiniryZimmerman09] Joseph Kiniry and Daniel Zimmerman. "A Verification-centric Software Development Process for Java". The 9th International Conference on Software Quality (QSIC 2009). Jeju, Korea. August, 2009.
- [ZimmermanNagmoti10] Dan Zimmerman and Rinkesh Nagmoti. "JMLUnit: The Next Generation". Formal Verification of Object-Oriented Software (FoVeOOS). Paris, France. June, 2010.
On program analysis
- Michael I. Schwartzbach: Lecture Notes on Static Analysis, BRICS research center, Uni. Aarhus.
- Claus Brabrand: How to Solve Recursive Equations (of monotone functions over lattices), ITU, April 3, 2008.
In the 2010 edition of the course, Joe's lectures were recorded and made available as podcasts.
Course project proposals
Project proposals will be presented in the Wednesday 6 April lecture 1200-1220.
Proposed by Peter Sestoft
- Project presentation slides from 6 April 2011
- Change the MicroC compiler to generate x86 code in the form of input for the NASM assembler.
- Extend the MicroC compiler to handle more of real C, such as struct types, switch, break, continue, malloc/free.
- Do a survey of Java or .NET virtual machine technology, for instance IBM JVM papers (Suganuma) and more recent work, Bak's contributions to Sun Hotspot, the Mono implementation, previous Smalltalk VM work and so on. Start with Aycock's survey from 2003.
- Write an interpreter -- in Scala, Standard ML, F#, Scheme, Java or C# -- for a substantial subset of the Icon language, or for SETL or another "unusual" language. See PLCSD chapter 11.
- Study garbage collectors for virtual machines, in particular Java and .NET; e.g. Bacon's recent work for the IBM JVM.
- Performance engineering for a managed platform (JVM, .NET) and modern x86 cpus. Consider either numeric intensive code (matrix multiplication), or object-intensive code such as the C5 collection library. Investigate bottlenecks using profiling, and experiment with alternative implementations and target platforms.
- Write a generator of specialized methods in C# (for instance, serialization and deserialization methods to XML or Json).
- Consider partial evaluation of spreadsheet-defined functions in the context described here (research).
- Here are some other project proposals, many of which are related to the course focus.
Proposed by David Christiansen (who cannot be a supervisor himself, but others may supervise)
- Use Scala's combinator parser library to write a parser for a substantial language, such as a subset of C# or Java, and produce some sort of interesting report (cyclomatic complexity as Joe talks about it, for example, or some other simple analysis - possibly generate a graphviz file showing class relationships).
- Implement a combinator parsing library in C#. (There's an embryonic one in Peter Sestoft's 2001 experiments with a research prototype of C# generics). Enable the use of LINQ for defining new parsers using the library. Take a look at Scala's combinator parers and their use of the for comprehensions for inspiration.
- Implement a basic version of a library such as QuickCheck or ScalaCheck for C#, again allowing the use of LINQ to define data generators in the same way that Haskell's do notation is used by QuickCheck and for comprehensions are used by ScalaCheck.
Proposed by Joe Kiniry
Project presentation slides from 6 April 2011
- BON IDE
- Connect the prototype BON IDE to BONc and/or improve the IDE.
- BON Model Metrics
- Investigate model metrics in the research literature and implement a static checker for them within BONc.
- Add support for refinement of informal BON to Javadoc, scenario and events to tests, creation to ownership, dynamic diagram to call analysis.
- Semantic Properties
- Extend the Propi system to include support for specification of semantics.
- Eiffel Type System
- Formalize a fragment of the Eiffel type system then analyze the Eiffel Studio compiler to see if it actually realizes this fragment.
- Contribute to the OpenJML system in any one of a number of ways.
- Verified Systems Development
- Perform rigorous analysis, design, development, validation, and verification of a system of your choosing.
See the Project Proposals section of my research group's website for other ideas.