Dictionaries

Usage:dictionary(D)

D is a dictionary.

Usage:dictionary(D,K,V,L,R)

The dictionary node D has key K, value V, left child L, and right child R.

• The following properties should hold upon exit:
  (dict:non_empty_dictionary/1)D is a non-empty dictionary.

Usage:dic_node(D,N)

N is a sub-dictionary of D.

• The following properties should hold at call time:
  (dict:non_empty_dictionary/1)D is a non-empty dictionary.
• The following properties should hold upon exit:
  (dict:dictionary/1)N is a dictionary.

Usage:dic_lookup(D,K,V)

D contains value V at key K. If it was not already in D it is added.

• The following properties should hold upon exit:
  (dict:non_empty_dictionary/1)D is a non-empty dictionary.

Usage:dic_lookup(D,K,V,O)

Same as dic_lookup(D,K,V). O indicates if it was already in D (old) or not (new).

• The following properties should hold upon exit:
  (dict:non_empty_dictionary/1)D is a non-empty dictionary.
  (dict:old_or_new/1)dict:old_or_new(O)

Usage:dic_get(D,K,V)

D contains value V at key K. Fails if it is not already in D.

• The following properties should hold at call time:
  (term_typing:nonvar/1)D is currently a term which is not a free variable.
  (dict:dictionary/1)D is a dictionary.
• The following properties should hold upon exit:
  (dict:non_empty_dictionary/1)D is a non-empty dictionary.

Usage:dic_replace(D,K,V,D1)

D and D1 are identical except for the element at key K, which in D1 contains value V, whatever has (or whether it is) in D.

• The following properties should hold at call time:
  (dict:dictionary/1)D is a dictionary.
  (dict:dictionary/1)D1 is a dictionary.
• The following properties should hold upon exit:
  (dict:dictionary/1)D is a dictionary.
  (dict:dictionary/1)D1 is a dictionary.

old_or_new(old).
old_or_new(new).

Usage:non_empty_dictionary(D)

D is a non-empty dictionary.