For a bit of context, this is a specification language built on top of Standard ML, and inspired by the Vienna Development Method. It supports iterative refinement of specifications, while keeping formal guarantees at each step. It was used by e.g. some railway traffic and satellite control systems in Scandinavia. I was part of one of those projects.
The RAISE book linked in the site, and previously published by Prentice Hall, is now freely available and describes quite a few small project examples. A very recent description and discussion of RAISE can be found in Dines Bjørner’s monograph Domain Science & Engineering.
For a bit of context, this is a specification language built on top of Standard ML, and inspired by the Vienna Development Method. It supports iterative refinement of specifications, while keeping formal guarantees at each step. It was used by e.g. some railway traffic and satellite control systems in Scandinavia. I was part of one of those projects.
The RAISE book linked in the site, and previously published by Prentice Hall, is now freely available and describes quite a few small project examples. A very recent description and discussion of RAISE can be found in Dines Bjørner’s monograph Domain Science & Engineering.