AutoProof Base Library API Reference
note
description: "Finite bags."
class interface
MML_BAG [G]
create
default_create,
singleton,
multiple
feature {NONE} -- Initialization
default_create
-- Create an empty bag.
singleton (x: G)
-- Create a bag that contains a single occurrence of `x'.
multiple (x: G; n: INTEGER)
-- Create a bag that contains `n' occurrences of `x'.
require
n_positive: n >= 0
feature -- Measurement
count alias "#": INTEGER_32
-- Total number of elements.
occurrences alias "[]" (x: G): INTEGER_32
-- How many times `v' appears.
feature -- Comparison
is_disjoint (a_other: MML_BAG [G]): BOOLEAN
-- Do `a_other' and `Current' have no elements in common?
is_equal (a_other: like Current): BOOLEAN
-- Is `a_other' the same bag as `Current'?
is_subbag alias "<=" (a_other: MML_BAG [G]): BOOLEAN
-- Does `other' contain all the elements of `Current'?
feature -- Convenience
empty_bag: MML_BAG [G]
-- Empty bag.
-- Can be used as `{MML_BAG [G]}.empty_bag'.
feature -- Iterable implementation
new_cursor: ITERATION_CURSOR [G]
-- Fresh cursor associated with current structure
feature -- Lemmas
lemma_remove_all (v: G)
-- Removing `Current [v]' occurrences of `v' from `b' is the
-- same as removing all occurrences.
ensure
removed_multiple (v, Current [v]) = removed_all (v)
lemma_remove_multiple (v: G; n: INTEGER_32)
-- Removing `n' occurrences of `v' from `Current' and then one,
-- is the same as removing `n' + 1 occurrences.
require
n >= 0
ensure
removed_multiple (v, n).removed (v) = removed_multiple (v, n + 1)
feature -- Modification
difference alias "-" (other: MML_BAG [G]): MML_BAG [G]
-- Current bag with all occurrences of values from `other' removed.
extended alias "&" (x: G): MML_BAG [G]
-- Current bag extended with one occurrence of `x'.
extended_multiple (x: G; n: INTEGER_32): MML_BAG [G]
-- Current bag extended with `n' occurrences of `x'.
require
n_non_negative: n >= 0
intersection alias "*" (other: MML_BAG [G]): MML_BAG [G]
-- Bag that contains only elements present in both
-- `other' and `Current'.
removed alias "/" (x: G): MML_BAG [G]
-- Current bag with one occurrence of `x' removed if present.
removed_all (x: G): MML_BAG [G]
-- Current bag with all occurrences of `x' removed.
removed_multiple (x: G; n: INTEGER_32): MML_BAG [G]
-- Current bag with at most `n' occurrences of `x' removed
-- if present.
require
n_non_negative: n >= 0
restricted alias "|" (subdomain: MML_SET [G]): MML_BAG [G]
-- Bag that consists of all elements of `Current'
-- that are in `subdomain'.
union alias "+" (other: MML_BAG [G]): MML_BAG [G]
-- Bag that contains all elements from `other' and `Current'.
feature -- Properties
has (x: G): BOOLEAN
-- Is `x' contained?
is_constant (c: INTEGER_32): BOOLEAN
-- Are all values equal to `c'?
is_empty: BOOLEAN
-- Is bag empty?
is_valid: BOOLEAN
-- Id `Current' a valid bag (are all occurrences non-negative)?
feature -- Sets
domain: MML_SET [G]
-- Set of values that occur at least once.
end -- class MML_BAG
note
description: "Closed integer intervals."
class
MML_INTERVAL
inherit
MML_SET [INTEGER]
create
from_range
feature {NONE} -- Initialization
from_range (l, u: INTEGER)
-- Create interval [l, u].
end
note
description: "Finite maps."
class interface
MML_MAP [K, V]
create
default_create,
singleton
feature {NONE} -- Initialization
default_create
-- Create an empty map.
note
maps_to: "Map#Empty"
singleton (k: K; x: V)
-- Create a map with just one key-value pair <`k', `x'>.
feature -- Measurement
count: INTEGER_32
-- Map cardinality.
feature -- Comparison
is_disjoint (a_other: like Current): BOOLEAN
-- Do `a_other' and `Current' have disjoint domains?
is_equal (a_other: like Current): BOOLEAN
-- Is `a_other' the same sequence as `Current'?
feature -- Conversion
domain: MML_SET [K]
-- Set of keys.
image (subdomain: MML_SET [K]): MML_SET [V]
-- Set of values corresponding to keys in `subdomain'.
require
in_domain: subdomain <= domain
range: MML_SET [V]
-- Set of values.
sequence_image (s: MML_SEQUENCE [K]): MML_SEQUENCE [V]
-- Sequence of images of `s' elements under `Current'.
require
range_in_domain: s.range <= domain
to_bag: MML_BAG [V]
-- Bag of map values.
feature -- Convenience
empty_map: MML_MAP [K, V]
-- Empty map.
-- Can be used as `{MML_MAP [K, V]}.empty_map'.
feature -- Elements
item alias "[]" (k: K): V
-- Value associated with `k'.
require
in_domain: domain [k]
feature -- Iterable implementation
new_cursor: ITERATION_CURSOR [K]
-- Fresh cursor associated with current structure
feature -- Modification
inverse: MML_RELATION [V, K]
-- Relation consisting of inverted pairs from `Current'.
override alias "+" (other: MML_MAP [K, V]): MML_MAP [K, V]
-- Map that is equal to `other' on its domain and to `Current'
-- on its domain minus the domain of `other'.
removed (k: K): MML_MAP [K, V]
-- Current map without the key `k' and the corresponding value.
-- If `k' doesn't exist, current map.
restricted alias "|" (subdomain: MML_SET [K]): MML_MAP [K, V]
-- Map that consists of all key-value pairs in `Current' whose
-- key is in `subdomain'.
updated (k: K; x: V): MML_MAP [K, V]
-- Current map with `x' associated with `k'.
-- If `k' already exists, the value is replaced, otherwise added.
feature -- Properties
has (x: V): BOOLEAN
-- Is value `x' contained?
is_constant (c: V): BOOLEAN
-- Are all values equal to `c'?
is_empty: BOOLEAN
-- Is map empty?
end -- class MML_MAP
note
description: "Finite relations."
class interface
MML_RELATION [G, H]
create
default_create,
singleton
feature {NONE} -- Initialization
default_create
-- Create an empty relation.
singleton (x: G; y: H)
-- Create a relation with just one pair <`x', `y'>.
feature -- Measurement
count: INTEGER_32
-- Cardinality.
feature -- Comparison
is_equal (a_other: like Current): BOOLEAN
-- Is `a_other' the same relation as `Current'?
feature -- Convenience
empty_relation: MML_RELATION [G, H]
-- Empty relation.
-- Can be used as `{MML_RELATION [G]}.empty_relation'.
feature -- Iterable implementation
new_cursor: ITERATION_CURSOR [G]
-- Fresh cursor associated with current structure
feature -- Modification
difference alias "-" (other: MML_RELATION [G, H]): MML_RELATION [G, H]
-- Relation that consists of pairs contained in
-- `Current' but not in `other'.
extended (x: G; y: H): MML_RELATION [G, H]
-- Current relation extended with pair (`x', `y') if absent.
intersection alias "*" (other: MML_RELATION [G, H]): MML_RELATION [G, H]
-- Relation that consists of pairs contained in both
-- `Current' and `other'.
inverse: MML_RELATION [H, G]
-- Relation that consists of inverted pairs from `Current'.
removed (x: G; y: H): MML_RELATION [G, H]
-- Current relation with pair (`x', `y') removed if present.
restricted alias "|" (subdomain: MML_SET [G]): MML_RELATION [G, H]
-- Relation that consists of all pairs in `Current' whose
-- left component is in `subdomain'.
sym_difference alias "^" (other: MML_RELATION [G, H]): MML_RELATION [G, H]
-- Relation that consists of pairs contained in either
-- `Current' or `other', but not in both.
union alias "+" (other: MML_RELATION [G, H]): MML_RELATION [G, H]
-- Relation that consists of pairs contained in either
-- `Current' or `other'.
feature -- Properties
has alias "[]" (x: G; y: H): BOOLEAN
-- Is `x' related `y'?
is_empty: BOOLEAN
-- Is map empty?
feature -- Sets
domain: MML_SET [G]
-- The set of left components.
image (subdomain: MML_SET [G]): MML_SET [H]
-- Set of values related to any value in `subdomain'.
image_of (x: G): MML_SET [H]
-- Set of values related to `x'.
range: MML_SET [H]
-- The set of right components.
end -- class MML_RELATION
note
description: "Finite sequence."
class interface
MML_SEQUENCE [G]
create
default_create,
singleton,
constant
convert
singleton ({G})
feature {NONE} -- Initialization
default_create
-- Create an empty sequence.
note
maps_to: "Seq#Empty"
singleton (x: G)
-- Create a sequence with one element `x'.
constant (x: G; n: INTEGER)
-- Create a sequence with n copies of `x'.
require
n_non_negative: n >= 0
feature -- Measurement
count alias "#": INTEGER_32
-- Number of elements.
occurrences (x: G): INTEGER_32
-- How many times does `x' occur?
feature -- Comparison
is_equal (a_other: like Current): BOOLEAN
-- Is `a_other' the same sequence as `Current'?
is_less_equal alias "<=" (a_other: MML_SEQUENCE [G]): BOOLEAN
-- If this sequence shorter than or the same length as `a_other'?
is_prefix_of (other: MML_SEQUENCE [G]): BOOLEAN
-- Is this sequence a prefix of `other'?
feature -- Conversion
domain: MML_SET [INTEGER_32]
-- Set of indexes.
range: MML_SET [G]
-- Set of values.
to_bag: MML_BAG [G]
-- Bag of sequence values.
to_map: MML_MAP [INTEGER_32, G]
-- Sequence viewed as a map from indexes to value.
feature -- Convenience
empty_sequence: MML_SEQUENCE [G]
-- Empty sequence.
-- Can be used as `{MML_SEQUENCE [G]}.empty_sequence'.
non_void: BOOLEAN
-- Does this sequence contain only non-Void elements?
feature -- Decomposition
but_first: MML_SEQUENCE [G]
-- Current sequence without the first element.
require
not_empty: not is_empty
but_last: MML_SEQUENCE [G]
-- Current sequence without the last element.
require
not_empty: not is_empty
first: G
-- First element.
require
non_empty: not is_empty
front (upper: INTEGER_32): MML_SEQUENCE [G]
-- Prefix up to `upper'.
interval (lower, upper: INTEGER_32): MML_SEQUENCE [G]
-- Subsequence from `lower' to `upper'.
last: G
-- Last element.
require
non_empty: not is_empty
removed_at (i: INTEGER_32): MML_SEQUENCE [G]
-- Current sequence with element at position `i' removed.
require
in_domain: domain [i]
tail (lower: INTEGER_32): MML_SEQUENCE [G]
-- Suffix from `lower'.
feature -- Elements
item alias "[]" (i: INTEGER_32): G
-- Value at position `i'.
require
in_domain: 1 <= i and i <= count
feature -- Iterable implementation
new_cursor: ITERATION_CURSOR [G]
-- Fresh cursor associated with current structure
feature -- Modification
concatenation alias "+" (other: MML_SEQUENCE [G]): MML_SEQUENCE [G]
-- The concatenation of the current sequence and `other'.
extended alias "&" (x: G): MML_SEQUENCE [G]
-- Current sequence extended with `x' at the end.
extended_at (i: INTEGER_32; x: G): MML_SEQUENCE [G]
-- Current sequence with `x' inserted at position `i'.
require
valid_position: 1 <= i and i <= count + 1
prepended (x: G): MML_SEQUENCE [G]
-- Current sequence prepended with `x' at the beginning.
replaced_at (i: INTEGER_32; x: G): MML_SEQUENCE [G]
-- Current sequence with `x' at position `i'.
require
in_domain: domain [i]
feature -- Properties
has (x: G): BOOLEAN
-- Is `x' contained?
is_constant (c: G): BOOLEAN
-- Are all values equal to `c'?
is_empty: BOOLEAN
-- Is the sequence empty?
end -- class MML_SEQUENCE
note
description: "Finite sets."
class interface
MML_SET [G]
create
default_create,
singleton
feature {NONE} -- Initialization
default_create
-- Create an empty set.
singleton (x: G)
-- Create a set that contains only `x'.
feature -- Measurement
count alias "#": INTEGER_32
-- Cardinality.
feature -- Comparison
is_disjoint (a_other: MML_SET [G]): BOOLEAN
-- Do no elements of `a_other' occur in `Current'?
is_equal (a_other: like Current): BOOLEAN
-- Is `a_other' the same set as `Current'?
is_subset_of alias "<=" (a_other: MML_SET [ANY]): BOOLEAN
-- Does `a_other' have all elements of `Current'?
is_superset_of alias ">=" (a_other: MML_SET [G]): BOOLEAN
-- Does `Current' have all elements of `a_other'?
feature -- Convenience
empty_set: MML_SET [G]
-- Empty set.
-- Can be used as `{MML_SET [G]}.empty_set'.
non_void: BOOLEAN
-- Are all elements non-Void?
feature -- Elements
any_item: G
-- Arbitrary element.
require
not_empty: not is_empty
max: G
-- Greatest element.
require
not_empty: not is_empty
min: G
-- Least element.
require
not_empty: not is_empty
feature -- Iterable implementation
new_cursor: ITERATION_CURSOR [G]
-- Fresh cursor associated with current structure
feature -- Modification
difference alias "-" (other: MML_SET [G]): MML_SET [G]
-- Set of values contained in `Current' but not in `other'.
extended alias "&" (x: G): MML_SET [G]
-- Current set extended with `x' if absent.
intersection alias "*" (other: MML_SET [G]): MML_SET [G]
-- Set of values contained in both `Current' and `other'.
removed alias "/" (x: G): MML_SET [G]
-- Current set with `x' removed if present.
sym_difference alias "^" (other: MML_SET [G]): MML_SET [G]
-- Set of values contained in either `Current' or `other',
-- but not in both.
union alias "+" (other: MML_SET [G]): MML_SET [G]
-- Set of values contained in either `Current' or `other'.
feature -- Properties
has alias "[]" (x: G): BOOLEAN
-- Is `x' contained?
is_empty: BOOLEAN
-- Is the set empty?
end -- class MML_SET
note
description: "Array with specification usable in AutoProof."
frozen class interface
SIMPLE_ARRAY [G]
create
make_empty,
make,
make_from_array
feature {NONE} -- Initialization
make_empty
-- Create an empty array.
ensure
empty_array: count = 0
make (n: INTEGER)
-- Create an array of size `n' filled with default values.
require
n_non_negative: n >= 0
ensure
count_set: count = n
all_default: across sequence.domain as i all sequence [i.item] = ({G}).default end
make_from_array (a: SIMPLE_ARRAY [G])
-- Create an array with the same elements as `a'.
require
a_non_void: a /= Void
ensure
same_elements: sequence = a.sequence
feature -- Access
count: INTEGER_32
-- Number of elements.
require
reads (Current)
ensure
definition: Result = sequence.count
item alias "[]" (i: INTEGER_32): G assign put
-- Item at position `i'.
require
in_bounds: 1 <= i and i <= count
valid_index: valid_index (i)
reads (Current)
ensure
definition: Result = sequence [i]
subarray (l, u: INTEGER_32): SIMPLE_ARRAY [G]
-- Subarray from `l' to `u' (inclusive).
require
l_not_too_small: l >= 1
u_not_too_large: u <= count
l_not_too_large: l <= u + 1
ensure
result_wrapped: Result.is_wrapped
result_fresh: Result.is_fresh
result_sequence_definition: Result.sequence ~ sequence.interval (l, u)
result_count_definition: Result.count = (u - l + 1)
feature -- Status report
has (v: G): BOOLEAN
-- Does the array contain `v'?
valid_index (i: INTEGER_32): BOOLEAN
-- Is `i' a valid index into the array?
require
reads (Current)
feature -- Modification
force (v: G; i: INTEGER_32)
-- Update value at position `i' with `v'.
require
in_bounds: 1 <= i and i <= count + 1
ensure
count_effect: (i = old count + 1) implies count = old count + 1
sequence_effect: (i = old count + 1) implies sequence = old sequence.extended (v)
count_effect: (i <= old count) implies count = old count
sequence_effect: (i <= old count) implies sequence = old sequence.replaced_at (i, v)
put (v: G; i: INTEGER_32)
-- Update value at position `i' with `v'.
require
in_bounds: 1 <= i and i <= count
valid_index: valid_index (i)
ensure
same_count: count = old count
sequence_effect: sequence = old sequence.replaced_at (i, v)
remove_at (i: INTEGER_32)
-- Remove element at position `i'.
require
in_bounds: 1 <= i and i <= count + 1
valid_index: valid_index (i)
ensure
count_reduced: count = old count - 1
sequence_effect: sequence = old sequence.removed_at (i)
feature -- Specification
sequence: MML_SEQUENCE [G]
-- Sequence of values.
invariant
count_definition: count >= 0 and count = sequence.count
end -- class SIMPLE_ARRAY
frozen class interface
SIMPLE_LIST [G]
create
make
feature {NONE} -- Initialization
make
-- Create an empty list.
ensure
empty: is_empty
feature -- Access
count: INTEGER_32
-- Number of elements in the list.
require
reads (Current)
ensure
definition: Result = sequence.count
has (x: G): BOOLEAN
-- Is `x' an element of the list?
require
reads (Current)
ensure
definition: Result = sequence.has (x)
is_empty: BOOLEAN
-- Is the list empty?
require
reads (Current)
ensure
definition: Result = sequence.is_empty
item alias "[]" (i: INTEGER_32): G
-- Element at index `i'.
require
in_bounds: 1 <= i and i <= count
reads (Current)
ensure
definition: Result = sequence [i]
feature -- Extension
extend_back (v: G)
-- Insert `v' at the back.
ensure
sequence_effect: sequence = old (sequence & v)
extend_front (v: G)
-- Insert `v' in the front.
ensure
sequence_effect: sequence = old (sequence.prepended (v))
feature -- Modification
put (v: G; i: INTEGER)
-- Update value at position `i' with `v'.
require
in_bounds: 1 <= i and i <= count
ensure
same_count: count = old count
sequence_effect: sequence = old sequence.replaced_at (i, v)
remove_at (i: INTEGER)
-- Remove element at position `i'.
require
in_bounds: 1 <= i and i <= count
ensure
count_reduced: sequence.count = old sequence.count - 1
sequence_effect: sequence = old sequence.removed_at (i)
feature -- Specification
sequence: MML_SEQUENCE [G]
-- Sequence of list's elements.
end -- class SIMPLE_LIST
