This directory contains a generic type class implementation of separation
algebra for Isabelle/HOL as well as lemmasand generic tactics which can be
used directly for any instantiation of the type class.
The ex directory contains example instantiations that include structures such
as a heap or virtual memory.
The abstract separation algebra is based upon "Abstract Separation Logic"by
Calcagno et al. These theories are also the basis of "Mechanised Separation Algebra"by Klein et al.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
Suchen
