SHARE
TWEET

Socrates

przemko Jun 18th, 2019 (edited) 111 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. procedure Main with SPARK_Mode is
  2.  
  3.    type Domain is new Integer with Ghost;
  4.  
  5.    Socrates : constant Domain := 0 with Ghost;
  6.  
  7.    function Human (X : Domain) return Boolean
  8.      with Ghost, Import;
  9.  
  10.    function Mortal (X : Domain) return Boolean
  11.      with Ghost, Import;
  12.  
  13. begin
  14.    pragma Assume (Human (Socrates));
  15.    pragma Assume (for all X in Domain => (if Human (X) then Mortal (X)));
  16.  
  17.    pragma Assert (Mortal (Socrates));
  18. end Main;
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top