Hello all, 

I thought the BlackBox community might be interested in this exchange  
on another interest group list for computer science educators. 

Stan 

Begin forwarded message: 

From: Stan Warford <Stan.Warford@pepperdine.edu> 
Date: December 10, 2003 1:06:05 PM PST 
To: "Hollingsworth, Joseph E" <jholly@ius.edu> 
Cc: Math-thinking@cs.geneseo.edu 
Subject: Re: comment on text books 

On Dec 10, 2003, at 12:13 PM, Hollingsworth, Joseph E wrote: 

[snip] 

The point here is, unless you're dealing with simple built-in types 
(e.g., integers, characters, Booleans, and possibly arrays and records 
of these types) it's not so easy to just introduce formal specs into 
a textbook and/or a computing class.  If you want to use abstractions 
that are more complex (e.g., stacks, queues, lists, maps, etc.) then you've 
got some work ahead of you.  And, it's probably not going to be 
very easy to retrofit mathematical abstractions and specifications back 
onto STL components or Java utility components.  So you end up growing 
your own component library.  I haven't seen Stan Warford's book using 
Component Pascal, but I'm guessing that this is what he had to do in order 
to support the some of the things that he wanted to do in his book. 

I did my own stacks and lists. However, the support for formal reasoning 
is provided in two places: (1) The Component Pascal Language has the 
ASSERT statement built in; it is not a library call. The trap mechanism 
when the assert fails produces a run-time stack window with hypertext 
links to the offending source code and easy-to-read variable values. 
(2) Every method provided by the BlackBox framework is documented 
with asserted pre- and post- conditions. It is natural to relate the 
online documentation to the Hoare Triple that students learn in the 
concurrent Discrete Structures class. It is also natural in this environment 
to teach the concept of loop invariants. Regardless of the practicality 
of formal methods in large commercial software projects, I agree 
with Scott that students from the beginning need to develop the 
mental tools for reasoning about programs in the small. Just two days 
ago I was helping a student in my office with loop invariants, and 
the light went on and he had that Aha experience. I believe he will 
be a better programmer for it. 

Stan 

J. Stanley Warford 
Professor of Computer Science 
Pepperdine University 
Malibu, CA 90263 
310-506-4332 
Stan.Warford@pepperdine.edu 

_______________________________________________ 
Math-thinking mailing list  -  Math-thinking@cs.geneseo.edu 
http://cs.geneseo.edu/mailman/listinfo/math-thinking ISTR