Development Log

  • SPARK Pro
    May 2nd, 2017

    Use unique names for simple private types
    For simple private types (untagged private type with no discriminants and full view out of SPARK) we now use unique names in Why3 so that they can easily be mapped to distinct existing types in interactive provers.