- Sep 28, 2019
-
-
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.
-
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.
-
Bart Wijgers authored
-
- Sep 27, 2019
-
-
Bart Wijgers authored
And merged it with the edited version we had. It seems that this extra line is the only thing that changed.
-
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).
-
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.
-
- Sep 21, 2019
-
-
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 :)
-
- Sep 20, 2019
-
-
Bart Wijgers authored
-
- Sep 18, 2019
-
-
Stoll,M. (Maximilian Stoll) authored
Extended the GCL Parser/Lexer to also parse/lex RepBy See merge request !1
-
Maximilian authored
-
- Sep 17, 2019
-
-
Bart Wijgers authored
-
- Sep 14, 2019
-
-
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.
-
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.
-