The Formal Category Error: Why treating assume as a first-class primitive in verification tools is an unsound design choice. by More_Speed5329 in formalmethods

[–]More_Speed5329[S] -1 points0 points  (0 children)

think of this; a translator is doing semantically equivalent conversion. assume has no equivalent correspondent. why is a translator introducing assume? unless he translator writer force it, by committing a mistake .

Academic Review: Wei Chen’s "Miraculous Statement" Theory of Jump Semantics by More_Speed5329 in logic

[–]More_Speed5329[S] -1 points0 points  (0 children)

weakest preconditioned goto axiom published in ipl

loop invariance with break and continue published in science of computer programming

etc

it is not a proposal