Isabelle/HOL-OCL

HOL-OCL Logo

HOL-OCL ist ein interaktives Beweissystem für die Object Constraint Language (OCL). HOL-OCL ist eine flache Einbettung von OCL in die Logik höhrer Ordnung (HOL) Instanz des interaktiven Theorembeweisers Isabelle. HOL-OCL wird von Achim D. Brucker und Burkhart Wolff entwickelt.

HOL-OCL screenshot

HOL-OCL erlaubt Beweise über OCL Spezifikationen zu führen, OCL Spezifikationen zu verfeinern und bietet die Grundlage für weitere Anwendungen, z.B. die automatische Test-Datensatz Berechnung.

HOL-OCL ist freie Software und kann unter den Bedingungen der GPL weitergegebenwerden und wird von Achim D. Brucker und Burkhart Wolff entwickelt.

Download

hol-ocl-0.9.0.tar.gz (ca. 4.6 MiB, MD5: a41aa55362108d8141ec4d901844cc08) ChangeLog

Publikationen

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2003

2002

2001