przemko

Socrates

Jun 18th, 2019
588
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

Adblocker detected! Please consider disabling it...

We've detected AdBlock Plus or some other adblocking software preventing Pastebin.com from fully loading.

We don't have any obnoxious sound, or popup ads, we actively block these annoying types of ads!

Please add Pastebin.com to your ad blocker whitelist or disable your adblocking software.

×