Linköping University Electronic Press: Electronic Articles: Computer and
Information Science
  ------------------------------------------------------------------------

A Floyd-Hoare Method for Prolog.

   Title: A Floyd-Hoare Method for Prolog.
 Authors: Wlodzimierz Drabent

  Series: Linköping Electronic Articles in Computer and Information Science
          ISSN 1401-9841
   Issue: Vol. 2(1997): nr 013
     URL: http://www.ep.liu.se/ea/cis/1997/013/
  ------------------------------------------------------------------------
 Abstract:We present an inductive assertion method for proving run-time
          properties of logic programs. The method could be seen as a logic
          programming counterpart of the well-known approach of Floyd and
          Hoare for imperative programs.
          The method concerns assertions assigned to program points and
          makes it possible to prove that whenever the control reaches a
          program point the corresponding assertion is satisfied.
          We also show a way of augmenting the method to prove termination.
          An assertion (assigned to a point in a program clause) describes
          a set of substitutions (for the variables of the clause).
          Assertions may be not monotonic (i.e. not closed under
          substitutions).
 Keywords:
  ------------------------------------------------------------------------
           Original Postscript Checksum
        publication
        1997-12-19
      Supplementary
   details from the
             author
       Miscellanous .
        information
  ------------------------------------------------------------------------
    [About LiEP] [About Checksum validation] [About compression formats]
  ------------------------------------------------------------------------
Editor-in-chief: editor@ep.liu.se     Last modified: Thu Dec 18 11:34:59 MET
Webmaster: webmaster@ep.liu.se                                         1997