The PYTHON_MAPPING tree

class interface PYTHON_MAPPING
   --  base class for python mapping mirror classes (dictionary)
creation
   make_from_borrowed_reference (new_python_object_pointer: POINTER)
      -- uses the given object pointer and increases the reference 
      -- count of the given python object.  Used in cases where the 
      -- Python C api does not automatically increase the reference 
      -- count.  Terminology ("borrowed reference" vs "new reference") 
      -- is taken from the Python C Api documentation
      require
         new_python_object_pointer.is_not_null
   make_from_new_reference (new_python_object_pointer: POINTER)
      -- uses the given object pointer without increasing reference 
      -- count of the python object.  Used because several Python C 
      -- api calls generate a new object with a reference count of 
      -- 1, and we don't want to increase that or we get too many 
      -- false references
      require
         new_python_object_pointer.is_not_null
   make_from_python_object (object: PYTHON_OBJECT)
      -- uses the existing python_object_pointer of python_object 
      require
         object /= Void
feature(s) from PYTHON_MAPPING
   length: INTEGER
      -- number of items in the mapping
      ensure
         last_python_integer_result_ok;
         last_python_integer_result_ok
   delete_item_string (key: STRING)
      -- deletes an item given a string key
      ensure
         last_python_integer_result_ok
   delete_item (key: PYTHON_OBJECT)
      -- deletes an item given a PYTHON_OBJECT key
      ensure
         last_python_integer_result_ok
   has_key_string (key: STRING): BOOLEAN
      -- whether or not the mapping contains an item with the given 
      -- string key
   has_key (key: PYTHON_OBJECT): BOOLEAN
      -- whether or not the mapping contains an item with the given
      -- PYTHON_OBJECT key
   keys: PYTHON_LIST
      --  list of keys in the mapping
   values: PYTHON_LIST
      -- list of values in the mapping
   items: PYTHON_LIST
      -- list of items in the mapping
   get_item_string (key: STRING): PYTHON_OBJECT
      -- gets the item stored with the given key
      require
         has_key_string(key)
   set_item_string (key: STRING; value: PYTHON_OBJECT)
      -- stores the value in the mapping under the given key
      ensure
         last_python_integer_result_ok
invariant
   reference_count >= 0;
   valid_reference: not is_none implies is_mapping;
end of PYTHON_MAPPING

class interface PYTHON_DICTIONARY
   -- encapsulation of python's dictionary class
creation
   make
      -- creates a new mapping
      ensure
         reference_count = 1
   make_from_new_reference (new_python_object_pointer: POINTER)
      -- uses the given object pointer without increasing reference 
      -- count of the python object.  Used because several Python C 
      -- api calls generate a new object with a reference count of 
      -- 1, and we don't want to increase that or we get too many 
      -- false references
      require
         new_python_object_pointer.is_not_null
   make_from_borrowed_reference (new_python_object_pointer: POINTER)
      -- uses the given object pointer and increases the reference 
      -- count of the given python object.  Used in cases where the 
      -- Python C api does not automatically increase the reference 
      -- count.  Terminology ("borrowed reference" vs "new reference") 
      -- is taken from the Python C Api documentation
      require
         new_python_object_pointer.is_not_null
   make_from_python_object (object: PYTHON_OBJECT)
      -- uses the existing python_object_pointer of python_object 
      require
         object /= Void
feature(s) from PYTHON_DICTIONARY
   make
      -- creates a new mapping
      ensure
         reference_count = 1
   clear
      -- clears dictionary of all key/value pairs
      ensure
         length = 0
   set_item (key, value: PYTHON_OBJECT)
      -- inserts value into the dictionary with key
      ensure
         last_python_integer_result_ok;
         last_python_integer_result_ok
   set_item_string (key: STRING; value: PYTHON_OBJECT)
      -- inserts value into dictionary with key
      ensure
         last_python_integer_result_ok;
         last_python_integer_result_ok
   delete_item (key: PYTHON_OBJECT)
      -- removes item with given key
      require
         has_key(key)
      ensure
         last_python_integer_result_ok;
         not has_key(key);
         last_python_integer_result_ok
   delete_item_string (key: STRING)
      -- removes item with given key 
      require
         has_key_string(key)
      ensure
         last_python_integer_result_ok;
         not has_key_string(key);
         last_python_integer_result_ok
   get_item (key: PYTHON_OBJECT): PYTHON_OBJECT
      -- gets item with given key
   get_item_string (key: STRING): PYTHON_OBJECT
      -- gets item with given key
      require
         has_key_string(key)
   keys: PYTHON_LIST
      -- list of keys
   items: PYTHON_LIST
      -- list of items in (key, value) tuples
   values: PYTHON_LIST
      -- list of values in dictionary
   length: INTEGER
      -- number of entries
      ensure
         last_python_integer_result_ok;
         last_python_integer_result_ok;
         last_python_integer_result_ok
invariant
   reference_count >= 0;
   valid_reference: not is_none implies is_mapping;
   valid_reference: not is_none implies is_dictionary;
end of PYTHON_DICTIONARY