RISC RISC Research Institute for Symbolic Computation  
  • @techreport{RISC3927,
    author = {Wolfgang Schreiner},
    title = {{How to Write Postconditions with Multiple Cases}},
    language = {english},
    abstract = {We investigate and compare the two major styles of writing program/ function postconditions with multiple cases: as conjunctions of implications or as disjunctions of conjunctions. We show that both styles not only have different syntax but also different semantics and pragmatics and give recommendations for their use.},
    year = {2009},
    month = {November},
    institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
    keywords = {formal methods, program specification, program verification},
    length = {3}