component Map is {
      state {
         map_info : \set MapInfo; 
         destinations : \set String;
      }
      invariant {
      }
      interface {
         prov ip1: SetDistance(start : String; end : String; 
                               distance : Integer);
         prov ip2: CalcDistance(start : String; end : String) : Integer;
      }
      operations {
         prov op1: {
            let  start : String;
                 end : String; 
                 dist : Integer;
                 map_info_dist : Integer;
            pre  (start \in destinations) \and (end \in destinations);
            post (map_info_dist = dist);
         }
         prov op2: {
            let  start : String;
                 end : String; 
                 map_info_dist : Integer;
            pre  (start \in destinations) \and (end \in destinations);
            post (\result = map_info_dist) \and
                 (~start \in destinations) \and 
                 (~end \in destinations);
         }
      }
      map {
         ip1 -> op1 (start -> start, end -> end, distance -> dist);
         ip2 -> op2 (start -> start, end -> end);
      }
   }