midspiral/lemmafit/lemmafit-dafny

include "Replay.dfy"
 
module CounterDomain refines Domain {
  // The model is the state of your application
  type Model = int
 
  // Actions are the ways the state can change
  datatype Action = Inc | Dec
 
  // Invariant: what must always be true about the state
  predicate Inv(m: Model) {
    m >= 0
  }
 
  // Initial state
  function Init(): Model {
    0
  }
 
  // How actions transform the state
  function Apply(m: Model, a: Action): Model {
    match a
    case Inc => m + 1
    case Dec => m - 1
  }
 
  // Normalization: fix invalid states (called after Apply)
  function Normalize(m: Model): Model {
    if m < 0 then 0 else m
  }
 
  // Proof that Init satisfies the invariant
  lemma InitSatisfiesInv()
    ensures Inv(Init())
  {
  }
 
  // Proof that every step preserves the invariant
  lemma StepPreservesInv(m: Model, a: Action)
    // requires Inv(m) is inherited and should not be repeated
    ensures Inv(Normalize(Apply(m, a)))
  {
  }
}
 
module CounterKernel refines Kernel {
  import D = CounterDomain
}
 
module AppCore {
  import K = CounterKernel
  import D = CounterDomain
 
  function Init(): K.History { K.InitHistory() }
 
  function Inc(): D.Action { D.Inc }
  function Dec(): D.Action { D.Dec }
 
  function Dispatch(h: K.History, a: D.Action): K.History requires K.HistInv(h) { K.Do(h, a) }
  function Undo(h: K.History): K.History { K.Undo(h) }
  function Redo(h: K.History): K.History { K.Redo(h) }
 
  function Present(h: K.History): D.Model { h.present }
  function CanUndo(h: K.History): bool { |h.past| > 0 }
  function CanRedo(h: K.History): bool { |h.future| > 0 }
}

function optimize(e: exp): exp
{
    match e
    case EInt(v) => e
    case EVar(x) => e
    case EAdd(e1, e2) => (match (optimize(e1), optimize(e2))
        case (EInt(0), e2) => e2
        case (e1, EInt(0)) => e1
        case (e1, e2) => EAdd(e1, e2))
}