******************************************************* Listing of SPARK Text SPARK95 Examiner with VC and RTC Generator Release 7.3 / 01.06 Demonstration Version ******************************************************* DATE : 09-MAR-2010 15:43:31.96 Line 1 with Stack; 2 --# inherit Stack; 3 --# main_program; 4 procedure MainInherit 5 --# global Stack.State; 6 --# derives Stack.State 7 --# from *; 8 is 9 I : Integer; 10 begin 11 -- Stack.Clear; 12 Stack.push(25); 13 Stack.pop(I); ^1 !!! ( 1) Flow Error : 10: Assignment to I is ineffective [Explanatory note: This message always relates to a procedure call or an assignment to a record. The variable XXX may be an actual parameter corresponding to a formal one that is exported; otherwise XXX is an exported global variable of the procedure. The message indicates that the updating of XXX, as a result of the procedure call, has no effect on any final values of exported variables of the calling subprogram. Where the ineffective assignment is expected (e.g. calling a supplied procedure that returns more parameters than are needed for the immediate purpose), it can be a useful convention to choose a distinctive name, such as "Unused" for the actual parameter concerned. The message "Assignment to Unused is ineffective" is then self-documenting.]. 14 -- Stack.Push(I); 15 end MainInherit; !!! ( 2) Flow Error : 33: The variable I is neither referenced nor exported. --End of file--------------------------------------------------