Diferencia entre revisiones de «Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)»

De WikiGLC
Saltar a: navegación, buscar
Línea 16: Línea 16:
 
|-
 
|-
 
| '''Code:'''  
 
| '''Code:'''  
−
| You can find the PVS (version 3.2) theories [http://www.cs.us.es/~mjoseh/pub/PROTEMO.tgz here] and (version 4.2) [http://www.cs.us.es/~mjoseh/pub/PROTEMO_4.2 here].
+
| You can find the PVS theories:
 +
* Version PVS-3.2 [http://www.cs.us.es/~mjoseh/pub/PROTEMO.tgz here]  
 +
* Version PVS-4.2 [http://www.cs.us.es/~mjoseh/pub/PROTEMO_4.2 here].
 
|-
 
|-
 
| '''Documentation:'''
 
| '''Documentation:'''

Revisión del 11:13 7 oct 2010

Title: Proving termination with multiset orderings in PVS: theory, methodology and applications
Authors: José A. Alonso, María J. Hidalgo and Francisco J. Martín.
Date: November 2009.
Description: This theory presents a methodology to organize and simplify non-trivial termination proofs of functions using well-founded multiset orderings. The theory consists of:
  1. A formalization of the theorem of Dershowitz and Manna.
  2. A methodology for proving termination properties.
  3. Three case studies: a tail-recursive definition of Ackermann's function, an iterative definition of McCarthy's 91 function and an iterative function to compute a generic schema for double recursion
Code: You can find the PVS theories:
  • Version PVS-3.2 here
  • Version PVS-4.2 here.
Documentation: Papers and documents related with this work:
Obtenido de «https://www.glc.us.es/web/index.php?title=Proving_termination_with_multiset_orderings_in_PVS:_theory,_methodology_and_applications_(PROTEMO)&oldid=984»