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

PENFOUND

VERSION

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

ORIGIN

ASSET

REVIEW CODE

OK

INET ADDRESS

librarian@source.asset.com

AUTHOR

Wolfgang Polak
UNISYS

RIGHTS

Approved for public release; distribution unlimited

COPYRIGHT

1994 UNISYS

LOCATION

ASSET
PAL

---

CLASSIFICATION

KEYWORDS

Penelope
Tasking
Software Measurement
Measurement, Software

INDEX

Polak, Wolfgang
Unisys

DEPENDENCIES

None

SEE ALSO

SHORT DESCRIPTION

A method utilizing process logic for verifying concurrent programs

TAXONOMY

Documents

Software Verification

Penelope

Logical Foundations

---

FILE LISTING

FILE SPECS

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

DIRECTORY DISPLAY

Follow path to see directory

---

ABSTRACT

Report on Logical Foundations for Penelope

This document presents a method, utilizing process logic, to specify and verify concurrent programs.

The Penelope Ada proof editor allows a user to incrementally develop provably correct Ada programs. The current version of the Penelope system is formally based on a predicate transformer semantics for sequential Ada. The purpose of this work is to provide the mathematical foundations for extending Penelope to Ada tasking programs.

Several issues need to be addressed to this end.

• A suitable logical formalism needs to be defined within which it is possible to reason about concurrent programs. In the case of sequential programs first-order logic was sufficient for this purpose.
• A specification and an annotation language must be defined for stating properties of concurrent programs. In the case of sequential programs input/output conditions and loop invariants are used as specifications.
• A method for defining the semantics of Ada needs to be devised. Given a program and a specification, it must be possible to derive conditions under which the program will satisfy it specifications. This step corresponds to the generation of verification conditions in the sequential case.
• An effective proof procedure must be found for showing that the correctness conditions generated for a program are true. If first-order logic is used, then a first-order theorem prover will suffice, in the concurrent case a theorem prover for a richer language will be needed.
• Finally, a new methodology for the systematic development of correct tasking programs needs to be developed. This includes ways to formally express problem specification, to find proper program annotations and so on.

This document addresses primarily the first three questions. While an appropriate notion of proof is formally defined within our mathematical framework, issues of the engineering of a practical theorem prover are not discussed. The use of the new formalism for proving the correctness of tasking programs is demonstrated with several programming examples. But the development of a verification methodology requires more extensive experience.

---

REVISION HISTORY

STARS-AC-A023/005/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)