Development Log

  • SPARK Pro
    Feb 24th, 2017

    Dynamic type constraints of protected components
    GNATprove now better tracks dynamic type constraints of protected components, such as dynamic bounds, predicates and invariants. This results in more automatic proof on protected operations or their callers, whenever types of protected components have some dynamic constraints.