simple_mml - Simple Eiffel Library

Overview

simple_mml provides immutable mathematical model types for use in Design by Contract specifications. These classes allow you to express precise postconditions using mathematical concepts like sets, sequences, bags, maps, and relations.

Adapted from ETH Zurich's base2 library, simple_mml is fully void-safe and SCOOP-compatible. The library uses [G -> detachable ANY] generic constraints to ensure compatibility with the model equality operator in void-safe mode.

The key insight is that model objects are transient—constructed within contract expressions from already-attached source data. They mirror safe structures for mathematical comparison, enabling postconditions like model |=| old model & x that precisely specify state changes.

Quick Start

class STACK [G -> detachable ANY]
feature
    model: MML_SEQUENCE [G]
        -- Mathematical model of stack contents.

    push (x: G)
            -- Push `x` onto stack.
        do
            -- implementation
        ensure
            model_extended: model |=| old model & x
        end

    pop
            -- Remove top element.
        require
            not_empty: not model.is_empty
        do
            -- implementation
        ensure
            model_reduced: model |=| old model.but_last
        end
end

Features

Model equality operator |=| for contract comparisons
Immutable types—all modifications return new objects
Full set/sequence/bag/map/relation operations
1-indexed sequences (Eiffel convention)
Design by Contract throughout
Void-safe implementation
SCOOP-compatible

API Reference

MML_MODEL

Base class providing model equality comparison.

Feature	Description
`is_model_equal alias "\|=\|"`	Model equality comparison
`model_equals (v1, v2)`	Compare two values for model equality

MML_SET [G]

Finite mathematical sets with unique unordered elements.

Feature	Description
`default_create`	Create empty set
`singleton (x)`	Create set containing only x
`has alias "[]" (x)`	Is x contained?
`count alias "#"`	Cardinality
`extended alias "&" (x)`	Set with x added
`union alias "+" (other)`	Set union
`intersection alias "*" (other)`	Set intersection
`difference alias "-" (other)`	Set difference

MML_SEQUENCE [G]

Finite mathematical sequences (ordered collections).

Feature	Description
`default_create`	Create empty sequence
`item alias "[]" (i)`	Value at position i
`count alias "#"`	Number of elements
`first, last`	First/last element
`extended alias "&" (x)`	Sequence with x appended
`concatenation alias "+" (other)`	Concatenate sequences
`but_first, but_last`	Remove first/last element

MML_BAG [G]

Finite mathematical bags (multisets with counted duplicates).

Feature	Description
`default_create`	Create empty bag
`occurrences alias "[]" (x)`	Count of x in bag
`count alias "#"`	Total element count
`extended alias "&" (x)`	Bag with one more x
`union alias "+" (other)`	Bag union (sum counts)

MML_MAP [K, V]

Finite mathematical maps (partial functions).

Feature	Description
`default_create`	Create empty map
`item alias "[]" (k)`	Value for key k
`domain`	Set of keys
`range`	Set of values
`updated (k, v)`	Map with k mapped to v
`override alias "+" (other)`	Override with other map

MML_RELATION [G, H]

Finite mathematical relations (multi-valued keys).

Feature	Description
`default_create`	Create empty relation
`has alias "[]" (x, y)`	Is x related to y?
`domain`	Set of left components
`image_of (x)`	Set of values related to x
`inverse`	Inverted relation

MML_INTERVAL

Integer ranges for sequence indexing.

Feature	Description
`from_range (l, u)`	Create interval [l, u]
`has alias "[]" (i)`	Is i in interval?
`lower, upper`	Bounds

Installation

Add to your ECF file:

<library name="simple_mml" location="$SIMPLE_LIBS/simple_mml/simple_mml.ecf"/>