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/