Maps: Issues and Examples

Maps

Maps: Concepts, Issues, and Designs

Total vs Non-Total

In the general notion of maps, map-apply is partial. For any given map M, there can be points x in (the general domain) Dom where (map-apply M x) is not defined. But Specware requires that all operations be total. We will call the subsort on which the function is total its Defined-Dom There are two general methods for converting non-total functions to total functions:

Restrict to subsort: Restrict the function to (the current) Defined-Dom
Extend to full domain: Extend Defined-Dom to Dom (by specifying values for the points in Dom but not in Defined-Dom)

(Partial) Maps

The restrict to subsort technique is used to handle non-totality: the subsort is named Defined-Domain; and, map-apply is restricted to Defined-Domain.
The constructors are empty-map and map-shadow
There is an operation undefine-at to undefine the map at a point.
There are two versions:
- Basic-Map which does not have a size operation
- Map which does have a size operation and, hence, imports NAT.

Total Maps

The constructors are map-const (map-constant) and map-shadow
There is no empty map

Maps: Examples

Subsort solution to non-totality: Template for the solution
(Full) Specs for partial maps: are in : partial-map.re
Spec for total maps: Is in: total-map

SpecWeb Index

Specs

Template for the subsort solution to non-totality of partial maps

The non-totality of map-apply on partial map M can be handled by introducing a subsort, called Defined-Dom, for pairs <M x> where (defined-at M x). map-apply is then restricted to Defined-Dom subsort.
Note: This not the full spec for partial maps; it is just enough to illustrate the Subsort solution to non-totality of map-apply for partial maps.

spec MAP is
  sorts Dom, Cod, Map, Defined-Dom
  sort-axiom Defined-Dom = (Map, Dom) | defined-at?

  %---------------------------------------------
  % basic operations

  op empty-map  : Map
  op map-shadow : Map, Dom, Cod -> Map

  constructors {empty-map, map-shadow} construct Map

  %---------------------------------------------
  % derived concepts

  op defined-at? : Map, Dom -> Boolean

  definition map-defined-at?-def of defined-at? is
    axiom (not (defined-at? empty-map x))
    axiom (iff (defined-at? (map-shadow M x1 y) x2)
	       (or (equal x1 x2)
		   (defined-at? M x2)))
  end-definition


  op map-apply : Defined-Dom -> Cod

  definition map-apply-def of  map-apply is
    axiom (implies (equal ((relax defined-at?) M-at-x)
		          <(map-shadow M x y) x>)
	           (equal (map-apply M-at-x) y))
  end-definition
 end-spec