Skip to main content

Stack

Reference for mo:core/Stack in the core library.

Stack<T> is a small immutable persistent-data-structure stack wrapper backed by BSeq.XSeq<T>. Its Spec.model translates the stack into a ghost Seq<T> so push/pop contracts can state exact sequence effects.

Import​

mo:core/Stack

Status​

  • Runtime module

Public API​

Types​

  • Stack

Modules​

  • Spec

Functions​

empty<T>() : Stack<T>​

Constructs the empty value for this module's data structure.

Contract

ensures result.size == 0;
ensures Seq.len<T>(Spec.model<T>(result)) == result.size;
ensures Spec.model<T>(result) == Seq.empty<T>();

Use when: code or specifications need this operation with the documented contract.

push<T>(stack : Stack<T>, value : T) : Stack<T>​

Returns or applies the corresponding update to the structure.

Contract

requires stack.size == Seq.len<T>(Spec.model<T>(stack));
ensures result.size == stack.size + 1;
ensures Seq.len<T>(Spec.model<T>(result)) == result.size;
ensures Spec.model<T>(result) == Seq.concat<T>(Spec.model<T>(stack), Seq.singleton<T>(value));

Use when: the postcondition must relate the updated value to the previous one.

peek<T>(stack : Stack<T>) : ?T​

Reads the requested value from the structure.

Contract

requires stack.size == Seq.len<T>(Spec.model<T>(stack));
ensures stack.size == 0 ==> result == null;
ensures stack.size > 0 ==> result == ?Seq.get<T>(Spec.model<T>(stack), (stack.size - 1) : Int);

Use when: reading this value is part of an implementation or postcondition.

pop<T>(stack : Stack<T>) : (?T, Stack<T>)​

Returns the updated collection or value described by the contract.

Contract

requires stack.size == Seq.len<T>(Spec.model<T>(stack));
ensures stack.size == 0 ==> (result.0 == null and result.1 == stack);
ensures stack.size > 0 ==>
(result.0 == ?Seq.get<T>(Spec.model<T>(stack), (stack.size - 1) : Int)
and result.1.size == stack.size - 1
and Seq.len<T>(Spec.model<T>(result.1)) == result.1.size
and Spec.model<T>(result.1) == Seq.take<T>(Spec.model<T>(stack), stack.size - 1));

Use when: the postcondition must relate the updated value to the previous one.

Spec Module​

Spec Functions​

model<T>(stack : Stack<T>) : Seq<T>​

Returns the abstract ghost model used by contracts and lemmas.

Contract

ensures result == BSeq.Spec.model<T>(stack.data);

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

Summary​

  • Runtime module under mo:core/Stack.
  • Exposes 4 public functions.
  • Includes 1 spec helpers in Spec.