|
What's New --
Look here regularly for postings
|
| 1/28
|
| • |
Instructions for uploading homework to SVN
[HTM], to be discussed in
Tuesday's lecture.
| | • |
In the AP's Around the World news summary in Today's IDS
contains an item that reads, in part,
"French bank Societe Generale said Sunday that a trader who
evaded all its controls to bet $73.5 billion ... on European markets
hacked computers and `combined several fraudulent methods' to
cover his tracks, ..."
|
|
| 1/24
|
| • |
Mr. Kim was the first to point out (rightly) that the PVS source file
G.pvs,
posted on 1/18, contains at least one invalid theorem,
p4,
that "does not make sense at all."
The file I intended to post was [PVS].
Note:
This is not an assigned problem. (but it is a
good "self test" to see if you assimilating what you have learned
so far).
G.pvs
sets up another pre-algebra problem and asks you to add
any lemmas that arise in the course of solving it.
The file I originally posted was a
previous student's incomplete attempt to develop a solution.
Perhaps it is illuminating to see an example of what other
students have done, or, at least, how they attempted to do it.
|
|
| 1/21
|
| • |
See the article
Computer failure `most likely' cause of accident
in TimesOnLine.
A student who follows up on this event
(the preliminary AAIB report is to be released in 30 days)
with a class presentation will receive credit for doing so.
|
|
| 1/18
|
| • |
A (possibly obsolete) graph of PVS strategies
[PDF]
| | • |
Small PVS theories we will look at, time permitting, in the next lecture:
th_PROP
[PVS];
th_Gb
[PVS],
[PRF]
| | • |
Another pre-algebra problem, which will not be assigned as homework
th_G
[PVS],
|
|
| 1/14
|
| • |
You may want to take an advance look at the
PVS source file
decisions.pvs
[PVS], which will be used in Tuesday's lecture.
You can step through the proofs by:
| (a) |
downloading the PVS proof file
decisions.prf
[PRF] into the working directory.
| | (b) |
Locating the cursor on any of the theorems
| | (c) |
invoking the PVS command
M-x x-step-proof
| | (d) |
entering
TAB 1 to
take one proof step.
|
|
|
| 1/10
|
| • |
The classroom for this class is now officially changed to LH035.
| | • |
You should receive a test message via my mailing alias. Tell me at
the next class if you did not get this message.
| | • |
My draft C241 textbook [PDF] contains background material relevent
in this class. Chapter 6 on the relationship between inductive types, structural induction, and
recursive definitions is helpful in understanding how mathematical models are formulated in PVS.
Chapter 8 is a brief introduction to formal logic, the concept of validity, and symbolic calculi (See,
in particular, the logic at the end of the chapter). Chapter 9 on proving sequential programs illustrates
how formal logic is extended for reasoining about programs.
|
|