Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Konferenzbeitrag

Generic System Support for Deductive Program Development

MPG-Autoren
/persons/resource/persons44047

Ayari,  Abdelwaheb
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44075

Basin,  David A.
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Ayari, A., & Basin, D. A. (1996). Generic System Support for Deductive Program Development. In T. Margaria, & B. Steffen (Eds.), Second International Workshop, TACAS'96: Tools and Algorithms for the Construction and Analysis of Systems (pp. 313-328). Berlin, Germany: Springer.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0014-ABDC-E
Zusammenfassung
We report on a case study in using logical frameworks to support the formalization of programming calculi and their application to deduction-based program synthesis. Within a conservative extension of higher-order logic implemented in the Isabelle system, we derived rules for program development that can simulate those of the deductive tableau proposed by Manna and Waldinger. We have used the resulting theory to synthesize a library of verified programs, focusing on sorting algorithms. Our experience suggests that the methodology we propose is well suited both to implement and use programming calculi, extend them, partially automate them, and even formally reason about their correctness.