PAL CARD CATALOG ENTRY

SHORT DESCRIPTION

A method utilizing process logic for verifying concurrent programs


MOVEMENT WITHIN THE PAL CARD CATALOG
Move to top-level taxonomy
Move to keyword list

ASSET PROFILE

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

FILE LISTING

Directory Display


languages/ada/docs/penelope/penfound:
  File Name                 Size
  ---------                 ----
  README                   2,337
  penfound.zip           150,633


Totals
  ==============  ==============
    2 Files              152,970

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.

   o  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.
    
   o  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.

   o  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.

   o  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.

   o  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.