IT-Universitetet i København
 
  Tilbage Kursusoversigt
Kursusbeskrivelse
Kursusnavn (dansk):Advanced Models and Programs (recap) 
Kursusnavn (engelsk):Advanced Models and Programs (recap) 
Semester:Efterår 2013 
Udbydes under:cand.it., softwareudvikling og -teknologi (sdt) 
Omfang i ECTS:15,00 
Kursussprog:Engelsk 
Kursushjemmeside:https://learnit.itu.dk 
Min. antal deltagere:2 
Forventet antal deltagere:8 
Maks. antal deltagere:0 
Formelle forudsætninger:This study activity is a brush up version of the course Advanced Models and Programmes. Students who have not been signed up for the course before, cannot expect to follow this activity.
In order to register for the course please contact course manager Jesper Bengtson jebe@itu.dk

Generally:

  • Solid knowledge of the Java and C# programming languages. (Knowledge of at least one more programming language, particulary a functional language like ML, Haskell, or Lisp, is helpful).

  • Basic knowledge of mathematical foundations of programming and program reasoning (i.e., the idea that we'll talk about sets, sequences, types, etc. does not scare you off).

  • Basic knowledge of model-driven development and the underlying idea of models, relating model to models, and relating models to code. For example, understanding the basics of UML or a similar modeling language, understanding how mathematical models like sequences and sets are used to specify algorithms, or understanding how an AST is an algebraic model for a programming language, is adequate background knowledge.


Knowledge of programming languages and foundations of computing as represented in the following courses:

  • Programming Languages Concepts and Implementation (SPLC)

  • Foundations of Computing: Discrete Mathematics (SGDM)

  • Foundations of Computing: Algorithms and Data Structures (SGDS)


These courses can be taken in parallel, though preferably they will have been completed prior to taking this course.

Additionally, material covered in the following courses complement that which this course covers, so taking them prior to this course helps, but taking them in parallel or after is permitted.

  • Model Driven Development (KF30)

  • Object Oriented Programming (OOP)

  • System Architecture and Security (SSAS)

 
Læringsmål:The course has two major 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 students are expected to be able to:

  • apply relevant methods and techniques in the chosen project,

  • argue for the overall design-decisions in, and correctness properties of, the project, and

  • relate the project to the underlying theory.

 
Fagligt indhold:The subject of the course is programming language foundations and technologies, with special attention to advanced technologies that are likely to influence software practice over the next ten years.

The contents of the course is structured in four themes.

1. Axiomatic Reasoning about Models and Programs

In particular, their pragmatic use in program design via model-driven development, implementation, validation, and verification.

The material and structure for this part of the course will come from Benjamin Pierce's Software Foundations course using the Coq proof assistant.

http://www.cis.upenn.edu/~bcpierce/sf/

https://coq.inria.fr/

2. Foundations of Type Systems

We will cover the foundations of typed programming languages using Benjamin Pierce's Types and Programming Languages book.

http://www.cis.upenn.edu/~bcpierce/tapl/

3. Verifying imperative programs

We will cover operational and axiomatic semantics of imperative programming languages. We will use Hoare Logic and Separation Logic to write specifications for and prove the correctness of imperative programs.

We will verify Java Programs using the Coq proof assistant and Kopitiam.
Kopitiam is an Eclipse plugin that integrates the standard Java development environment with Coq, allowing programs and their proofs of correctness to be developed in one framework.

https://itu.dk/research/tomeso/kopitiam/

4. Rigorous Software Engineering and Testing

In particular, the concepts, tools, and techniques used for analysis and design of programs, one example being QuickCheck for Java.

http://quickcheck.java.net/ 
Læringsaktiviteter:

The course period is 16 weeks half time (15 ects). The course consists of:


  • Exercises (approximately 8 weeks), covering the themes of the course.

  • A project done in groups of 1-3 students (approximately 8 weeks), within one of the themes, resulting in a project report.



Note that there are no lectures associated with this course. It is intended to be taken by students who have not completed the Advanced Models and Programs course earlier. Help will still be provided, but this will be either by mail correspondence or by booking meetings with the teacher. Regular physical meetings can not be expected, but e-mail assistance will always be provided. 
Obligatoriske aktivititer:The weekly exercises must be handed in, and at least 80% of the exercises must be approved to pass the course.

The project must be completed

The students must pass an oral exam, where questions may be asked in all areas of the course. 
Eksamensform og -beskrivelse:X. experimental examination form (7-scale; external exam), 7-trins-skala, Ekstern censur

The weekly exercises must be handed in, and at least 80% of exercises must be approved to pass the course. The project report must be presented in an oral exam, where questions may be asked in all themes of the course.

The duration of this oral exam is 30 minutes.  

Litteratur udover forskningsartikler:Software Foundations by Benjamin Pierce 
 
Afholdelse (tid og sted)
Kurset afholdes på følgende tid og sted:
UgedagTidspunktForelæsning/ØvelserStedLokale
08.00-09.50 Forelæsning ITU Kurset kører kun online

Eksamen afholdes på følgende tid og sted:
EksamensdatoTidspunktEksamenstypeStedLokale
2013-12-11 No later than 2PM Skriftlige arbejder ITU Student Affairs and Programmes, 3D wing
2014-01-10 contact course manager Mundtlig eksamen ITU 4A22