map.key

Abstract datatype of (untyped) partial maps.

Author: Daniel Bruns
Documentation added by Alexander Weigl weigl@kit.edu

Sorts

Map

Map;defined in: map.key Line: 13 Offset :4

Functions

mapGet

Return a value from the given Map. If value is undefined, mapUndef is used.

/*! Return a value from the given Map. If value is undefined, `mapUndef` is used. */ any mapGet ( Map , any ) ; defined in: map.key Line: 19 Offset :4

mapUndef

A unique value, which is returned by mapGet in case no mapping value is declared for the specified key.

 /*! A unique value, which is returned by mapGet in case no mapping value is declared for the specified key. */ \unique any mapUndef  ;

defined in: map.key Line: 22 Offset :4

mapForeach

Generalized quantifier for maps. This is a generic constructor for maps.

KeY Logic Documentation

Defined symbols in the KeY System