ASE2 CARD CATALOG ENTRY

Instructions:

• Scroll forward and backward through this Card Catalog Entry to view it.
• Strike the PRINT button on your browser to print this Card Catalog Entry.
• Go to the FILE SPECS section of this Card Catalog Entry to find out where the associated directories and files are. If they are on this Website, you can transfer to them by clicking on the indicated hyperlinks. Note: the FILE SPECS hyperlink in this bullet will take you directly to the FILE SPECS section.
• Use the FIND command of your browser to search this Card Catalog Entry.
• Click here to go to the Card Catalog Taxonomy.
• Click here to go to the Card Catalog Index. Warning: the index file is large, so this may take a while on slower systems.
• Click here to go to the Title Page.

---

ASSET OVERVIEW

UNIT NAME

PENRM

VERSION

STARS-AC-A023/004/00, 26-FEB-94

ORIGIN

ASSET

REVIEW CODE

OK

INET ADDRESS

librarian@source.asset.com

AUTHOR

Carla Marceau
UNISYS

RIGHTS

Approved for public release; distribution unlimited

COPYRIGHT

1994 UNISYS

LOCATION

ASSET
PAL

---

CLASSIFICATION

KEYWORDS

Penelope
Software Measurement
Measurement, Software
Tasking

INDEX

Marceau, Carla
Unisys

DEPENDENCIES

None

SEE ALSO

SHORT DESCRIPTION

Reference manual for Penelope, an interactive environment for verification

TAXONOMY

Documents

Software Verification

Penelope

Reference Manual

---

FILE LISTING

FILE SPECS

Click here to enter Asset Directory/transfer Asset File(s): ../../ase02_01/docs/penelope/penrm

DIRECTORY DISPLAY

Follow path to see directory

---

ABSTRACT

Penelope Reference Manual

Penelope is an interactive environment that helps its user to develop and verify programs written in a rich subset of sequential Ada. Penelope is well-suited to developing programs in the goal-directed style advocated by Gries and Dijkstra. In this style the programmer develops a program from a specification in a way that ensures the program will meet the specification. Of course, Penelope can also be used to verify previously written programs. Sometimes we have to modify a completed program. With Penelope, it is often possible to verify a modified version of a program with minimal effort, by replaying and modifying the original program's proof.

This manual documents the language and commands of the Penelope environment. It is intended for the Penelope user, who desires to write specifications, develop programs, and carry out correctness proofs using Penelope. The user is assumed to be an Ada programmer with a strong mathematical background. A working knowledge of predicate calculus is essential. Even with such a background, the user may require the assistance of a trained mathematician for the more demanding aspects of Penelope, notably providing consistent axiomatic definitions of functions used in the specifications, organizing the proofs of the verification conditions, and proving lemmas needed during the verification. Chapter 2 documents how to get Penelope running. In order to develop and verify programs using Penelope, though, you will need to understand Penelope's approach to formal verification and to simplification and theorem proving.

---

REVISION HISTORY

STARS-AC-A023/004/00  1 June 94  Initial release to the PAL

---

RELEASE NOTICE

Approved for public release; Distribution unlimited

---

DISCLAIMER

This documentation is provided "AS IS" and without any expressed or
implied warranties whatsoever.  No warranties as to performance,
merchantability, or fitness for a particular purpose exist.
The user must assume the entire risk and liability of using this
document.  In no event shall any person or organization of people be
held responsible for any direct, indirect, consequential or
inconsequential damages or lost profits.

---

ASE CARD CATALOG ENTRY NAVIGATION

• Go to Title Page
• Go to Taxonomy
• Go to Index (warning: the index file is large, so this may take a while on slower systems)
• Go to Top of this Page

Powered by the Generic Web-Based Reuse Library (GWRL)