Software Saturdays: 05/18/2019
An introduction to (Floyd-)Hoare Logic, a logical framework for software specifications, that demonstrates use through a formal proof of a exponentiation function. Specification are structured in triplets of propositional logic statements called Hoare Triples composed of p, a precondition, c, a computation, q, a postcondition. The notation varies depending on the kind of specification declares. Total correctness statements are articulated [p]c[q], partially correct statements {p}c{q}. The difference between the two centers around termination, whole total correctness implies c’s termination given p’s validity, partially correct does not, decoupling c’s termination with p’s validity, instead asserting that q is implied if c terminates and p is valid.
Information Hiding as a paradigm for encapsulation. Basically, when looking at functionality thinking of the implementation in terms of what the public shouldn’t worry about. A well develop example that was used was and auto ID increment. Starts off as an incrementation and definition statement (newId: int = ++currID: int) but then requires changes like changing int to str, and instead of just changing declarations, using an IDTYPE alias to refer to whatever type is needed, as well as hiding the ID creation behind some sort of function/interface. Asking what to hide might help find reasonable designs when thinking about objects/classes might overburden the initiative.
A rather ethical take on the idea of software verification, i.e. the idea that in some automated way a system can determine correct. The argument uses exploits the weaknesses of abstraction to highlight the inherent flaws of modelling as the core reasons why verification is a misleading and immoral term, that relative consistency would be more apt. Relative consistency because correctness verification, for example, as expressed in Hoare Logic, is theoretically dependent on the on defined (pre|post)conditions and pragmatically dependent on the measurable strengths of these propositions. Measuring here, being another articulation of modelling, thus the approach is deeply plagued by the inevitable partiality of any projection (model) of any infinite space (reality).
.back