Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!wuarchive!uunet!mcsun!ukc!newcastle.ac.uk!turing!ncmh From: Chris.Holt@newcastle.ac.uk (Chris Holt) Newsgroups: comp.object Subject: Re: Readability of Ada Message-ID: <1991May12.173838.698@newcastle.ac.uk> Date: 12 May 91 17:38:38 GMT References: <1991May1.041007.14124@odi.com> <1991May9.040947.28053@netcom.COM> > for Current_Day in Monday..Friday loop >> Go_To_Work; >> end loop; Hmm... A loop is an optimized tail recursion, it seems to take an implicit argument Current_Day, drawn from a set. Except that the set is really a sequence. I assume ForAll is not intended, so a parallel implementation would be inappropriate? Because I'd want either ForAll Current_Day in {Monday..Friday} . Go_To_Work or Current_Day := Monday; Loop:: If Current_Day > Friday Then skip Else Begin Go_To_Work; Next(Current_Day); Loop End; these are both easier to verify from where I'm sitting. >> while Batter_Remains_In_Bowl and People_Are_Still_Hungry loop >> Make_More_Pancakes; >> end loop; Assuming nothing stupid like side-effects, my only problem would be how the functions in the condition are represented; people being hungry would seem to require a fuzzy domain, and the batter might be enough for a small but not a large pancake. In particular, the case of a person saying, "Well, okay, I'll have the last one just to use up the batter" seems hard to treat. This is not trivial; interactions between conditions like that can often arise. >> if You_Are_Sleepy then >> Go_To_Sleep; >> end if; This is a very imperative approach; presumably, if not sleepy then fall through the command to whatever follows. But putting it in other terms, we have (You_Are_Sleepy => Go_To_Sleep; continuation) or (not(You_Are_Sleepy) => continuation) and a proof of correctness would prefer this. So my summary would be, how easy is it to prove that these constructs satisfy their specifications? I accept that this was not the question being addressed, but even when minor notational changes are allowed for, it has an effect on readability. ----------------------------------------------------------------------------- Chris.Holt@newcastle.ac.uk Computing Lab, U of Newcastle upon Tyne, UK ----------------------------------------------------------------------------- "And when they die by thousands why, he laughs like anything." G Chesterton