Skip to content
Snippets Groups Projects
  1. Sep 28, 2019
    • Bart Wijgers's avatar
      Add calculation for WLPs from ProgramPaths · 930ad801
      Bart Wijgers authored
      Additionally, refactor some code to give everything its own space.
      Mainly, put any code that renames/substitutes variables in expressions
      into its own module (WLP.RenameFunctions).
      
      Note that not ALL programs in the mandatory part are done yet! We still
      need Array assignment, mostly.
      930ad801
    • Bart Wijgers's avatar
      Add "normalizeProgramPath" to WLP.ProgramPath · 65f242ec
      Bart Wijgers authored
      Some functions seem to assume that the program paths are formed by a
      fully left-associative application of the Seq constructor (as in: Seq
      Skip $ Seq Skip $ ... $ Seq Skip Skip). Therefore, this function is
      added; it will turn any string of Seq'ed statements into this shape.
      Using this function will do no harm (other than possibly spending effort
      into doing nothing), so use it accordingly.
      65f242ec
    • Bart Wijgers's avatar
      742b3815
  2. Sep 27, 2019
    • Bart Wijgers's avatar
      Update the parser · 2b05625d
      Bart Wijgers authored
      And merged it with the edited version we had. It seems that this extra
      line is the only thing that changed.
      2b05625d
    • Bart Wijgers's avatar
      Update examples · 55e161b6
      Bart Wijgers authored
      Some examples had syntax errors; those have been fixed. Additionally,
      I added a simple example with a while loop. It does not contain a proper
      post-condition either, which might be interesting as well (as the
      program might be able to handle those properly too).
      55e161b6
    • Bart Wijgers's avatar
      Calculate program paths · b2bf15c6
      Bart Wijgers authored
      This change allows us to calculate program paths from all programs (as
      long as they don't contain any try-catch). Using this, we should be able
      to calculate ALL wlps for the programs. However, the checks are not
      complete for the whole program, as only program paths up to a certain
      length are checked. Any further program paths might say that the program
      is (in)correct and give a different result.
      b2bf15c6
  3. Sep 21, 2019
    • Bart Wijgers's avatar
      Add basic WLP calculation · 961efaec
      Bart Wijgers authored
      The WLP of a subset of statements in the language can now be calculated.
      This needs to be extended, but it gives a basic idea of what we can do.
      
      I made new types for the logical expressions (and the mathematical
      expression in them) rather than reusing the datatype within the
      language. I feel that there's a benefit to separating these, showing
      when we're talking about the programs and when we're talking about the
      wlp and its calculation and the like. However, this does increase the
      amount of types we use. I think the benefit outweighs the cost of having
      extra types, but I also feel like we should discuss this :)
      961efaec
  4. Sep 20, 2019
  5. Sep 18, 2019
  6. Sep 17, 2019
  7. Sep 14, 2019
    • Bart Wijgers's avatar
      Add a .gitignore file · 71679cd4
      Bart Wijgers authored
      In case anyone wants to use a sandbox, this should make sure that is not
      being pushed. Also makes sure the build is not pushed.
      71679cd4
    • Bart Wijgers's avatar
      Initial Commit · ab2184f2
      Bart Wijgers authored
      Comes with a .cabal file that says to use z3, but you gotta install it
      first. This is *kind of* involved and so we should just do that
      together.
      ab2184f2
Loading