-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
402ad4f
commit b16dcbe
Showing
4 changed files
with
35 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
*~ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,32 @@ | ||
# pasv | ||
The Pascal-F Verifier | ||
|
||
The Pascal-F Veriifer is an early proof-of-correctness system. | ||
It was developed between 1982 and 1985 and works on a dialect | ||
of Pascal used for real-time programming. | ||
|
||
It ran on UNIX 4.x BSD on early VAX and Sun systems in the 1980s. | ||
The plan is to bring it back to life as a milestone in the history | ||
of program verification. | ||
|
||
The manual is here: | ||
|
||
http://www.animats.com/papers/verifier/verifiermanual.pdf | ||
|
||
## Original copyright notice | ||
|
||
Permission is hereby given to modify or use, but not for profit, | ||
any or all of this program provided that this copyright notice | ||
is included: | ||
|
||
Copyright 1985 | ||
|
||
Ford Motor Company | ||
The American Road | ||
Dearborn, Michigan 48121 | ||
|
||
This work was supported by the Long Range Research Program of | ||
the Ford Motor Company, and was carried out at Ford Scientific | ||
Research Labs in Dearborn, Michigan and Ford Aerospace and | ||
Communications Corporation's Western Development Laboratories | ||
in Palo Alto, California. |
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
# Original sources | ||
These are the original sources for the Pascal-F verifier, | ||
as stored in 1986. The file is in Macintosh Stuffit format. | ||
It can be unpacked under Linux with the "unar" program. |