AMP-Spring2010

From PLSwiki

Jump to: navigation, search

This is the course page for Advanced Models and Programs (SASP), spring 2010.

Contents

Practical and administrative matters

Teachers

Support

Questions about the course contents, particularly the second half focusing on dependable software development, should be asked in the AMP Blog.

Format

The course starts on Monday 25 January 2010 at 0830.

In the first week, we meet Monday 25 January 0830-1030 in room 2A18 and on Friday 29 January 1100-1300 in room 2A14. After that first week, the plan is as follows:

  • Monday 0830-1030 in room 4A16 and 1045-1245 in room 2A52
  • Friday 1100-1300 in room 2A14 and 1345-1545 in room 2A52

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.

Week-to-week exercises

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 List of Approved Weekly Exercises.

Final project

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 List of Project Submissions.

Examination

UPDATE 2010-06-08 Here is the exam schedule version 3. The exam takes place in auditorium 4 on Tue 15 June and in room 3A18 on Wed 16 June. Both rooms have projector, a laptop, and blackboard.

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

and

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

UPDATE 2010-05-03 Here is the exam syllabus, or "pensum", the material in which we may ask questions in addition to the project:

For the meaning of the paper references below, see the Literature and Materials section of this course homepage.

  • The Scala tutorial
  • Overview of the Scala Programming Language
  • Mogensen: Basics of compiler design, DIKU 2009, sections 2.1-2.9 and 3.1-3.6.
  • Coco/R User Manual pages 1-17, 23-28
  • Sestoft: Programming Language Concepts for Software Developers, chapters 1, 2, 3, 7, 8, 9, 10, 14
  • Kernighan and Ritchie: The C programming language, chapter 5.
  • Sestoft: Numeric performance in C, C# and Java, 2010
  • Dybvig: The Scheme Programming Language, MIT 2003, sections 2.1-2.7, 6.1
  • WaldenNerson94 chapters 1-8
  • BurdyEtal02
  • LeavensBakerRuby99
  • LeavensEtAl00
  • LeavensEtAl05
  • CheonLeavens02
  • KiniryCok04
  • ChalinEtAl05
  • KiniryZimmerman08
  • KiniryZimmerman09
  • Schwartzbach: Lecture notes on static analysis, chapters 1-6
  • All lectures slides
  • All mandatory exercises
  • In addition the following materials are "kursorisk pensum", that is, relevant background material but not something we will be asking detailed questions about in the oral exam: PaigeOstroffFM99, PaigeOstroffUML99, JanotaGrigoreMoskal07, LeavensCheon06

Exam date

CHANGE The oral exam will take Tuesday 15 June and Wednesday 16 June 2010. This is to ensure that we can use the same external examiner as previous years.

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.

Course content

Themes

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

Plan

Week Date Teacher Topic Materials Assignments
04 Mon 25 Jan PS C# vs Java: non-virtual methods, properties, indexers, operator overloading, value types, enum types, reference parameters. Slides PS1 Sestoft: C# Precisely, MIT Press 2005, or any later C# book, or online materials Assignment 1
Fri 29 Jan PS C# vs Java: iterator blocks, generic types and methods, anonymous methods, C# 3.0: inferred types, extension methods, ... Slides PS2 and Slides PS3 Sestoft: C# Precisely, MIT Press 2005, or any later C# book, or online materials
05 Mon 1 Feb PS C# 3.0: anonymous objects, object and collection initializers, Linq; default parameters, named arguments, variance in type parameters, the type dynamic C# 3.0 language specification, 2007 (MS Word format) Assignment 2
Fri 5 Feb PS Scala: object-oriented and functional programming combined, traits, ... Slides PS4 Read the Scala tutorial and the Overview of the Scala Programming Language (links below), or, if you get really excited, get the book Odersky, Spoon, Venners: Programming in Scala, Artima 2008
06 Mon 8 Feb PS Abstract syntax, interpretation and checking; lexing and parsing ... Slides PS5 Mogensen sections 2.1-2.9 and 3.1-3.6. Sestoft PLCSD chapters 1-3. Assignment 3
Fri 12 Feb PS Grammar transformations, compilation and stack machines ... Slides PS6 Coco/R User Manual pages 1-17, 23-29. Sestoft PLCSD chapters 1-3 and 8.2.
07 Mon 15 Feb PS Micro-C and pointers. Slides PS7 Kernighan and Ritchie chapter 5. Sestoft PLCSD chapters 7-8. Assignment 4
Fri 19 Feb PS Bytecode, abstract machines, and real machines. Slides PS8 Sestoft PLCSD chapters 9-10. Sestoft: Numeric performance in C, C# and Java. Ecma-335 CLI standard, partition I, section 12.3.
08 Mon 22 Feb PS Scheme, multi-stage programs Slides PS9 Dybvig sections 2.1-2.7, 6.1. Sestoft PLCSD chapter 14. Assignment 5
Fri 26 Feb PS Partial evaluation, runtime code generation. Slides PS10 Sestoft PLCSD chapter 14.
09 Mon 1 Mar PS Student presentations of several interesting languages: Python by Rasmus; and Erlang by Matyas; and F# by Sune; and Haskell by David. Assignment 6
Fri 5 Mar JK Background, Business Object Notation, and Analysis (Example Projects, Effective Use of Formal Methods, The Business Object Notation, Dependable Systems Analysis) Slides JK1 PaigeOstroffFM99, PaigeOstroffUML99, Chapters 1, 2, 6, 7, and 8 of WaldenNerson94
10 Mon 8 Mar JK Specifications (Assertions and Specifications, Contracts and Specifications in BON and JML) Slides JK2 Chapters 3, 4, 5 of WaldenNerson94, BurdyEtal02
Fri 12 Mar JK JML (Introduction to JML, Applying BON to Java and JML), Static Analysis (Code Standards and Metrics, Static Analysis for Software Construction) Slides JK3 Slides JK-JML LeavensBakerRuby99, LeavensEtAl00, LeavensCheon06, LeavensEtAl05 Assignment 7
11 Mon 15 Mar JK Validation (Testing, Types of Testing, Unit Testing, Testing in Practice, Testing with Specifications) Slides JK5 CheonLeavens02
Fri 19 Mar JK Verification (Kinds of Verification, Details of a Verification Tool, Model Checking, Using Verification Effectively) Slides JK6 KiniryCok04, ChalinEtAl05, JanotaGrigoreMoskal07, KiniryZimmerman08, KiniryZimmerman09 Assignment 8
12 Mon 22 Mar JK Using ESC/Java2, Models in JML, Hints and Tips for Verification Slides JK7 JK8 JK9
Fri 26 Mar JK No lecture, only lab session. Assignment 9
13 Mon 29 Mar Easter
Fri 2 Apr Easter
14 Mon 5 Apr Easter
Fri 9 Apr JK 1100-1125 Project proposal presentations. 1125- Undecidability, Static Analysis, Data-Flow Analysis, and Control-Flow Graphs. Slides Lecture Notes Chapters 1, 2, and 5; i.e., pages 3-6 + 15-17.
15 Mon 12 Apr JK "Extraterrestrial Mathematics" (which we need for Data-Flow Analysis) Slides How to solve recursive equations Lecture Notes Chapter 4; i.e., pages 11-15. Assignment 10
Fri 16 Apr JK Data-flow Analyses in practice; we'll study examples. Slides Lecture Notes Chapter 6; pages 17-19 + 28-32.
16 Mon 19 Apr Projects
Fri 23 Apr Projects
17 Mon 26 Apr Projects
Fri 30 Apr Projects
18 Mon 3 May Projects
Fri 7 May Projects
19 Mon 10 May Projects
Fri 14 May Projects
20 Mon 17 May Projects
Fri 21 May Projects
21 Mon 24 May Project reports must be handed in no later than 15:00 on Tuesday 25 May

Literature and materials

Lecture Recordings

Recordings of Joe's lectures are now being made available as podcasts via the temporary URL: http://www.itu.dk/stud/mediabase/public/podcast/2010/BON/index.html

On C# 3.0 and 4.0 and Scala

On compilation and abstract machines

On program analysis

On the Business Object Notation

On the Java Modeling Language (JML) and Verification

Course project proposals

Project proposals will be presented in the Friday 9 April lecture 1100-1125.

Proposed by Peter Sestoft:

  • Project presentation slides from 9 April 2010
  • 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 Claus Brabrand:

  • Make a Data-Flow Analysis and implement it such that it can analyze (and optimize) programs written in (a subset of) some familiar language (e.g., Java, C#, ...)
  • Slide with proposal

Proposed by Joe Kiniry:

Proposed by Andrzej Wasowski:

Retrieved from "http://www.itu.dk/research/pls/wiki/index.php/AMP-Spring2010"
Personal tools