-
Notifications
You must be signed in to change notification settings - Fork 3
Specifications
We aim to use the dependent types and the proof checker of Coq to show some properties on the impure part of concurrent programs. Pure parts can already by proven using classical methods, even if there should be interesting things to do there too.
We know the programs are well-typed because the type system of Coq is supposed sound and because there are no unsafe operators (like Obj.magic).
All exceptions are caught since they must be explicitly typed in a monad. We use the simple error-handlers library to handle exceptions.
Depending on the interface with the OS we have different termination properties. Of course pure terms terminate. In general, except if there are infinitely many messages sent on a channel, impure programs either terminate or block, waiting for a message.
We could find operators to describe execution traces. The traces are not deterministic but have some structure: for example, each handler is executed sequentially and answers to a request can only arrive after the request itself.
The idea would be to do something in the way of Idris.
A specification could be viewed as an operating system playing against the program, and trying to make it fail. We need to allow the user to describe the behavior of the system, and show properties on a combined execution of the system plus the program.