******************************************************* Listing of SPARK Text SPARK95 Examiner with VC and RTC Generator Release 7.3 / 01.06 Demonstration Version ******************************************************* DATE : 28-FEB-2010 12:06:45.83 Line 1 package ND_RandomNumbers 2 is 3 procedure Random(X : out Float); 4 --# derives X 5 --# from ; 6 end ND_RandomNumbers; --End of file--------------------------------------------------