Package edu.udel.cis.vsl.sarl.prove.why3

package edu.udel.cis.vsl.sarl.prove.why3

Class	Description
RobustWhy3ProvePlatform
RobustWhy3ProvePlatformFactory
Why3ConcurrentRunner
Why3PermutTranslator	A translation of permut(a, b, l, h) predicate, where a, b are arrays and l, h are integral bounds.
Why3Primitives	This class provides a set of Why3 primitives, including types and operations, to help the translation.
Why3Primitives.Axiom
Why3Primitives.Why3Lib	Libraries in Why3.
Why3TranslationState	This class manages all stateful informations that are needed during the translation from SARL to Why3.
Why3Translator	Translates SARL SymbolicExpressions to the why3 (logic) language of the verification platform Why3 ( why3-website).