1. 10 Sep, 2015 1 commit
  2. 09 Sep, 2015 1 commit
  3. 07 Sep, 2015 2 commits
  4. 02 Sep, 2015 1 commit
  5. 01 Sep, 2015 1 commit
  6. 30 Aug, 2015 2 commits
  7. 29 Aug, 2015 1 commit
    • MARCHE Claude's avatar
      TryWhy3: first skeleton · d3373d05
      MARCHE Claude authored
      compile it with make src/trywhy3/trywhy3.js
      
      run it by loading src/trywhy3/index.html in your favorite browser
      
      first issue to solve : loading of standard library
      d3373d05
  8. 05 Aug, 2015 1 commit
    • David Hauzar's avatar
      Introducting constants with model labels for variables in the term · 0b53e050
      David Hauzar authored
      triggering VC.
      
      - Transformation intro_vc_vars_counterexamp introduces new constant with
      model labels for every variable in the term that trigger VC and axiom
      that this constant is equal to the variable, finds the position of the
      term that trigger VC, and saves this position in meta (for smtv2
      printer).
      
      - Transformation prepare_for_counterexmp additionally performs the
      transformation intro_vc_vars_counterexamp
      
      - smtv2 printer no longer collects the location of the term that
      triggers VC and does not collect variables in this term in a special
      way. Note that this functionality was not yet completely removed from
      the printer. It will be done so after the transformation
      intro_vc_vars_counterexmp will be tested.
      
      The rationale:
      Variables that should be displayed in counterexample are marked
      by model labels ("model", "model_projected", "model_trace:*").
      
      Variables inside the term that triggers VC should be displayed in
      counterexample for that VC. However, many VCs (tasks) can be generated
      for  a signle *.mlw file and only variables in the term that trigger
      the VC (task) that is currently proven should be displayed. That means
      that the process of selecting variables inside the term that triggers
      VC for counterexample must be done while processing the task. It is
      done by transformation intro_vc_vars_counterexmp. This means that smtv2
      printer no longer has to find the position of the term that triggers
      VC and no longer has to collect variables in this term in a special
      way.
      0b53e050
  9. 18 Jul, 2015 1 commit
  10. 17 Jul, 2015 1 commit
  11. 10 Jul, 2015 3 commits
  12. 02 Jul, 2015 1 commit
  13. 01 Jul, 2015 1 commit
  14. 26 Jun, 2015 1 commit
  15. 19 Jun, 2015 1 commit
  16. 18 Jun, 2015 1 commit
  17. 16 Jun, 2015 1 commit
  18. 12 Jun, 2015 2 commits
  19. 05 Jun, 2015 1 commit
  20. 02 Jun, 2015 1 commit
  21. 01 Jun, 2015 1 commit
  22. 29 May, 2015 2 commits
  23. 28 May, 2015 2 commits
  24. 18 May, 2015 1 commit
  25. 13 May, 2015 2 commits
  26. 30 Apr, 2015 1 commit
  27. 29 Apr, 2015 1 commit
  28. 23 Apr, 2015 1 commit
  29. 13 Apr, 2015 1 commit
    • David Hauzar's avatar
      Transformation that for each declared abstract function and predicate · 9b6d889c
      David Hauzar authored
      p labeled with label "model_projected" for that it exists a projection
      function f creates declaration of new constant c and axiom stating that
      c = f p
      
      Projection functions are functions tagged with meta "model_projection".
      Function f is projection function for abstract function and predicate p
      if f is tagged with meta "model_projection" and has a single argument
      of the same type as is the type of p.
      
      This transformation is needed in situations when we want to display not
      value of a variable, but value of a projection function applied to a variable.
      
      Note that since Why3 supports namespaces (different projection functions
      can have the same name) and input languages of solvers typically not,
      Why3 renames projection functions to avoid name clashes.
      This is why it is not possible to just store the name of the projection
      function in a label and than query the solver directly for the value of
      the projection.
      Also, it means that this transformation should thus be executed before
      this renaming.
      9b6d889c
  30. 02 Apr, 2015 1 commit
  31. 25 Mar, 2015 2 commits