Skip to content
Snippets Groups Projects
  • Bart Wijgers's avatar
    961efaec
    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
    History
    Add basic WLP calculation
    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 :)