Development Log

  • SPARK Pro
    Apr 23rd, 2012

    New proof statement for system assumptions
    A new proof statement (assume) has been added to introduce assumptions about a system. In essence, this can be used to introduce any fact into the proof system and is intended as a replacement for certain prv files. An example assumption could be "we reboot this system every 10 years, hence the uptime counter cannot overflow".