Our method relies on a parametric representation of an algebraic notion. One instantiation by a concrete operational structure as parameter results in an executable instance of the algebraic notion. A further instantiation by a symbolic parameter provides a way for proving properties of the new symbolic instance based on the properties of the given one.
We illustrate this method by examples taken from the implementation of various number systems in SML. The symbolic structures are completed by various semantic proof methods which allow to prove or disprove restricted classes of formulae. All provided methods are decidable, i.e. work automatically. We propose this case study as a possible benchmark for other approaches.
