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{([at]})nowhere.xy
Date: December 10, 2003 1:06:05 PM PST
To: "Hollingsworth, Joseph E" <jholly{([at]})nowhere.xy
Cc: Math-thinking{([at]})nowhere.xy
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{([at]})nowhere.xy
_______________________________________________
Math-thinking mailing list - Math-thinking{([at]})nowhere.xy
http://cs.geneseo.edu/mailman/listinfo/math-thinking
Received on Wed Dec 10 2003 - 22:53:11 UTC