Models, Algebras and Logic of Engineering Software

ACL2 algebra algorithm Alloy assertion atoms axioms basic behavior binary relation binding bytecode call stack components composed system composition concurrent programs condition cons constraints construction declarative declarative programming defined definition defthm defun denote equational logic example execution expression finite formal function heap Hoare Hoare Logic Hoare triple implementation induction input int-fix interface abstraction Java Kripke structure labels List machine mathematical Maude method model checking module morphisms NeList notation object operand stack operations pop stack postcondition predicate programming language proof property refinement prove pushout reachable relation requirements result rev L2 rev V#0 rewrite theory rewriting logic rules satisfies semantics sequence sequential signature specification stack top-frame th step structure symbols system model temporal logic theorem thread tool transition transition relation translation tuple variables verification