Abstract data type
Abstract variable

An abstract variable may be regarded as the simplest non-trivial ADT, with the semantics of an imperative variable. It admits two operations, fetch and store. Operational definitions are often written in terms of abstract variables. In the axiomatic semantics, letting V {\displaystyle V} be the type of the abstract variable and X {\displaystyle X} be the type of its contents, fetch is a function V → X {\displaystyle V\to X} and store is a function of type V → X → V {\displaystyle V\to X\to V}. The main constraint is that fetch always returns the value x used in the most recent store operation on the same variable V, i.e. fetch(store(V,x)) = x. We may also require that store overwrites the value fully, store(store(V,x1),x2) = store(V,x2).

In the operational semantics, fetch (V) is a procedure that returns the current value in the location V, and store (V, x) is a procedure with void return type that stores the value x in the location V. The constraints are described informally as that reads are consistent with writes. As in many programming languages, the operation store (V, x) is often written V ← x (or some similar notation), and fetch (V) is implied whenever a variable V is used in a context where a value is required. Thus, for example, V ← V + 1 is commonly understood to be a shorthand for store (V, fetch (V) + 1).

In this definition, it is implicitly assumed that names are always distinct: storing a value into a variable U has no effect on the state of a distinct variable V. To make this assumption explicit, one could add the constraint that:

This definition does not say anything about the result of evaluating fetch (V) when V is un-initialized, that is, before performing any store operation on V. Fetching before storing can be disallowed, defined to have a certain result, or left unspecified. There are some algorithms whose efficiency depends on the assumption that such a fetch is legal, and returns some arbitrary value in the variable's range.
startend:end_checker