Module Abstraction

module Abstraction: sig .. end
Shape-value abstraction of assertions


This module implements shape-value abstraction, which includes an adaptation of Distefano's simple list segment domain and custom abstractions for possibly sorted sequences and multiset values.

References:


type abs_options 
val add_imp_vars : string -> unit
val add_sorted_from : string -> unit
val default_options : abs_options
val sorting_options : abs_options
val valB_options : abs_options
val valA_valB_options : abs_options
val mk_abstraction : abs_options -> Assertions.prover -> Genarith.abstraction
Main entry point.

Configuration parameters & statistics


val prover_calls : int Pervasives.ref
Number of calls to the theorem prover during abstraction
val verbose : int Pervasives.ref
val args : (Arg.key * Arg.spec * Arg.doc) list
Imprint | Data protection