Re: Interested in Formal Methods

[Atle]

a hafiz wrote:
> 
> Hello,
> 
> i share your interest in Formal Methods and especially in applying it to
> HURD.  I have heard of VDM and B but not actually read about them let
> alone use them. But i did do  some Z while in Uni. and although it was
> difficult at first but once you get it, it's not too bad and i started
> to like it! i thought Z was fun! (maybe something wrong with me...)
This is what hapens! The most commercially used, and most standardized formal 
method is VDM-SL, which is also closer to 'normal'
mathematics :-). And you are right about the fun, there is NOTHING like seing 
your system specified mathematically by YOU! That
gives a satisfaction much greater than implementing and testing (or course it 
works, it has to!)
> 
> but then i was applying zed on simple exercises and relatively small
> programming projects ( < 5000 lines of code). and even then i didn't
> do it too well or apply it to rigorously. if i were too apply Zed to
> HURD i'd probably change my mind.
Currently, I use a programming language called BETA (www.mjolner.com) - there 
are certain things you can not do with this language,
and every time I came into one of those 'barriers' I discovered a semantic 
error in my program, or an error in the data. The same
with Math: If it doesn't 'add up' there is something wrong with it.
> 
> Anyway, i'd be very inerested in any work on applying Formal Method to HURD
> but i can't help you right now.
I know, I can barely help myself. I put my faith in the tutors I will have on 
my new winter course, they are generally amongst the
most knowledgeable in the area of formal methods :-)
> 
> Jason More, had a valid point about the whole thing. Formal Method can be
> very hard, and the amount of effort expended to apply it to HURD may not
> be worth the small gain. it might still be interesting and fun though!
I said I was not going to respond to this, so I can't respond, only as that 
people check this for themselves.
If you have an opinion on this, make sure you have read enough about it to be 
sure that you are right.
> so IF i were to do it, it would be just for the heck of it and hopefully
> there would be some sort of academic value to it, so it won't be a complete
> waste. I have actually toyed with the idea myself but not knowing much about
> Zed or OS design, it just remains an interest for me.
Had I been proficient in VDM-SL now, I may have gotten a job to design the new 
Joint Strike Force Fighter, they asked for VDM-SL.
So, if the bomb my home town or Oslo, I could have proudly said:"I build that!"
> 
> as far as concurrency in Zed, although Zed does not support concurency
> directly, you could still write a Zed spec to specify concurrency problems.
> You could also combine Zed and CSP in the same specification document. so
> i don't think it's a big issue. there might even be a conccurent Zed
> developed by now.
Also in VDM-SL, I think. If you know Z, you will have no problems with VDM-SL.
> 
> finally, my personal opinion on formal methods is that, it is not so
> much the method or notation, but it is what the method or notation forces
> you to do. What formal methods does is force you to think about your design
> a bit more thoroughly and it guides you to do it correctly. when you just
> draw some design base on some simple specs you tend to just do a quick
> sketch and straight away jump to the coding. with formal methods, you are
> more likely to expand your original idea, and explore the problem a little
> more.
You said it better than me :-)
Since BNF came into use, how much compiler syntax is specified in Ebglish, or 
with boxes and labels?