1package Protected_Func with SPARK_Mode is
2   protected Prot_Obj is
3      function Prot_Func return Integer;
4   private
5      Comp : Integer := 0;
6   end Prot_Obj;
7
8   Part_Of_Constit : Integer := 0 with Part_Of => Prot_Obj;
9end Protected_Func;
10