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
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