ASE2 CARD CATALOG ENTRY

Instructions:


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
You are on CDROM ID ase02_01
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

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