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 <[EMAIL PROTECTED]> 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?
_______________________________________________
Help-hurd mailing list
[EMAIL PROTECTED]
http://mail.gnu.org/mailman/listinfo/help-hurd
