From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,b438e75ce5e32099
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news4.google.com!news2.volia.net!news.germany.com!news.belwue.de!kanaga.switch.ch!switch.ch!newsserver.news.garr.it!newsserver.cilea.it!docenti.ing.unipi.it!o2943499
From: Colin Paul Gloster <Colin_Paul_Gloster@ACM.org>
Newsgroups: comp.lang.ada
Subject: Re: Generating Ada from UML on Linux
Date: Thu, 10 Aug 2006 19:06:54 +0200
Organization: CILEA
Message-ID: <20060810185748.M22459@docenti.ing.unipi.it>
References: <87ejvs6fj6.fsf@nbi.dk>
 <20060809130000.J84175@docenti.ing.unipi.it>
 <m2hd0k97q7.fsf@hugin.crs4.it>
Reply-To: Colin Paul Gloster <Colin_Paul_Gloster@ACM.org>
NNTP-Posting-Host: docenti.ing.unipi.it
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
X-Trace: newsserver.cilea.it 1155229615 7935 131.114.28.20 (10 Aug 2006
 17:06:55 GMT)
X-Complaints-To: news@cilea.it
NNTP-Posting-Date: 10 Aug 2006 17:06:55 GMT
X-X-Sender: o2943499@docenti.ing.unipi.it
In-Reply-To: <m2hd0k97q7.fsf@hugin.crs4.it>
Xref: g2news2.google.com comp.lang.ada:6158
Date: 2006-08-10T17:06:55+00:00
List-Id: <comp.lang.ada>

On Thu, 10 Aug 2006, Jacob Sparre Andersen wrote:

"[..]

Which formal specification language would you suggest for teaching
undergraduate students?  I am open to suggestions.  [..]"

I am not sure which to suggest, a number of them also have weaknesses and 
I do not know all of the good specification languages. VDM (specifically 
VDM-SL) can be represented in ASCII but it has no reuse capability 
whatsoever (e.g. it is not possible to write in VDM
predicate_p := some really long expression which will appear many times
predicate_q := some really long expression which will appear many times
predicate_r := some really long expression which will appear many times
if predicate_p and predicate_q
--...
elsif predicate_p or predicate_r
--...
else
--...). Z has this basic capability but is not expressible in ASCII (some 
people write it in LaTeX but LaTeX can easily need several runs before 
all interdependant references are resolved but still produces output 
which if not thoroughly checked could be mistaken for a finished 
document). Also, Z does not have any built-in temporal facilities.

Being an Ada course, the SPARK specification language might not be 
irrelevant.