Design Calculi for Telecommunications	Course Descriptions	Software Project Management Course	UNU-IIST Home
Advanced RAISE Course

II/2/1/4 Advanced RAISE Course

The main aim of the course is to teach the use of justification in RAISE. Hence the emphasis is practical with plenty of exercises, and the theoretical part is reduced to introductory explanations (plus reading material).

The exercises need to be done using the RAISE justification tools, with participants working in groups of 2/3 people. Access to tools is essential.

A basic knowledge of RSL is assumed. Ideally, participants should have attended the course Formal Software Specification Using RAISE II/2/1.

The course lasts one week, i.e. 10 3-hour sessions.

Topics

• Semantic background:

  • static semantics

  • denotational semantics

  • operational semantics

  • axiomatic semantics

  • the RAISE logic

  • convergence

• What should be proved?

  • confidence conditions

  • implementation relations

  • theorems

  • justification versus proof

• Introduction to justification:

  • equivalence rules

  • inference rules

  • applicability conditions

  • contexts

  • proof rule meta language

• Using context information:

  • axioms

  • definitions -- unfolding and folding

  • subtypes

• Induction:

  • natural induction

  • variant and record induction

• Structuring justifications:

  • lemmas

  • case analysis

  • theories

• Proof techniques:

  • forwards reasoning

  • contradiction

• Imperative justification:

  • applicability conditions

  • evaluation ordering

  • assignment propagation

  • always application

  • in-goal application

  • loops

• Concurrent justification:

  • normal forms

  • expansion rules

• Avoiding justification:

  • correctness by construction

  • applicative to imperative development

  • sequential to concurrent development

  • concurrent to distributed development

Advanced RAISE Course
Design Calculi for Telecommunications	Course Descriptions	Software Project Management Course	UNU-IIST Home