[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Formal methods?
|
From: |
David Welch |
|
Subject: |
Re: Formal methods? |
|
Date: |
Fri, 1 Dec 2000 16:45:47 +0000 (GMT) |
On Fri, 1 Dec 2000, Atle wrote:
>
> In February I will take a course about large projects, with an OS as a
> case study. There is one guy, teacher of formal methods, Georges
> Mariano <georges.mariano@inrets.fr> who will specify Linux in Z or B,
> and with some help I might have a go at a Hurd subsystem.
>
> But I will need help from someone who really knows the module,
> prefereably the author or maintainer. And nothing will be 'obvious' or
> 'self-explanatory' - everything has to be specified down to the most
> 'insignificant' detail, with domain specification, codomain (range),
> pre-conditions, post-conditions, invariants for data and loops,
> reification from a high level of abstraction down to bit-level ... a
> BIG, BIG job!!!
>
I don't know about VDM or B, but Z isn't designed to specify concurrent
programs. How will you handle this?