While I certainly agree in principle, in practice it is not currently
possible to teach SPARK in CS1 - There is no suitable textbook.
One of my summer plans is to write a 2nd edition of my "Ada Plus Data
Structures" textbook. I would like to include SPARK annotations in it
where possible. But it will still be Ada since I can't do a data
structures book without covering pointers. And it will be CS2 not CS1.
John
-----Original Message-----
>From: Team Ada: Ada Programming Language Advocacy (83 & 95)
>[mailto:[log in to unmask]] On Behalf Of Rod Chapman
>Sent: Friday, December 03, 2004 1:58 AM
>To: [log in to unmask]
>Subject: Re: The question at hand:
>
> You can also make a good case for teaching SPARK:
> 1) All the "good things" about Ada also apply (even more so)
> to SPARK.
> 2) SPARK teaches design-by-contract and strong program verification.
> 3) SPARK is _much_ smaller and simpler than Ada.
> 4) You can sell the idea to your curriculum committee without
> mentioning Ada!
>
> - Rod
John W. McCormick [log in to unmask]
Computer Science Department
University of Northern Iowa voice (319) 273-6056
Cedar Falls, IA 50614-0507 fax (319) 273-7123
http://www.cs.uni.edu/~mccormic/