AMP-Spring2011

From PLSwiki

Jump to: navigation, search

This is the course homepage for Advanced Models and Programs (SASP), spring 2011.

Contents

Practical and administrative matters

News

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.

Teachers

  • 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

Support

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.

Format

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.

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 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);

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

Examination

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


Exam date

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.

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

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.

Week Date Teacher Topic Materials Assignments Workload
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
PaigeOstroffFM99, PaigeOstroffUML99, Chapters 1, 2, 6, 7, and 8 of WaldenNerson94

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
Chapters 3, 4, 5 of WaldenNerson94, BurdyEtal02

 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

Slides JK3 Example Arch Spec

8+8+7 h
Wed 23 Mar JK Static Analysis (Code Standards and Metrics, Static Analysis for Software Construction)  Slides JK4

Static Analysis Demo Screencast
Semantic Static Checking Demo Screencast
AutoGrader Demo Screencast

13 Mon 28 Mar JK  Validation (Testing, Types of Testing, Unit Testing, Testing in Practice, Testing with Specifications)  Slides JK5
CheonLeavens02, ZimmermanNagmoti10 		Assignment 8,

hand-in Monday, 4 April

8+8+7 h
Wed 30 Mar JK Verification (Kinds of Verification, Details of a Verification Tool, Model Checking, Using Verification Effectively) Slides JK5

Example Validation Workspace
KiniryCok04, ChalinEtAl05, JanotaGrigoreMoskal07, KiniryZimmerman08, KiniryZimmerman09

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

On compilation and abstract machines

On the Business Object Notation

On the Java Modeling Language (JML) and System Validation and Verification


On program analysis

Lecture Recordings

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.
Beetlz
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.
OpenJML
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.

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