- Has the definition of “statistical mechanics” changed from its original meaning?
- Rotational Kinematics question about wheel
- Energy quantization of double symmetric square-well potential
- How to measure the average potential energy of air atoms in gravitational field?
- How can I achieve small field of view by 2 or more lenses?
- Do piezo materials change volume?
- Set Warranty Bit : Kernel help
- android correct screen size and density
- How to publish private apps?
- Select my own ringtone on Samsung s7 but only Sound picker is available
- How can I change the default camera app (on lockscreen)?
- How to drain LiFePO4 battery?
- RC time constant in circuit with two caps with different potential
- 7-segment display BCD decoder with normal hex values
- Beacon testing Microchip RN4871
- analog PWM signal
- Detecting human body current with raspberry pi
- 4bit demultiplexer with address entries in the EXCESS-3 code
- Sending List via JSON - Coding Structure Issue!
Inference rules for deriving invariants in Hoare logic
The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string):
X = S1
Y = S2
E = true
// (1) S1 = S2 <=> X = Y and E = true
while X != /\ and Y != /\ and E == true
if head(X) == head(Y)
X = tail(X)
Y = tail(Y)
E = false
// (2) S1 = S2 <=> X = /\ and Y = /\ and E = true
if !(X == /\ and Y == /\)
E = false
// (3) S1 != S2 and E = false
else // an empty else
// (3') S1 = S2 <=> E = true
// (4) S1 = S2 <=> E = true
There are five invariants:
(1). $S_1 = S_2 \iff X = Y \land E = true$
(2). $S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true$
(3). $S_1 \neq S_2 \land E = false$
(3'). $S_1 = S_2 \iff E = true$
(4). $S_1 = S_2 \iff E = true$
I can understand these invariants and how they are derived from the previous ones in an intuitive and thus informal way. For example, we can derive (3') from (2) as follows:
At point (2), we know that $S_1$ equals $S
There are two ways to answer the question.
The first is on the level of propositional logic. You have three statements, $S_1=S_2$, $(X=\Lambda\wedge Y=\Lambda)$, and $E=true$. Let's call them $A$, $B$, and $C$ for short. (2) is $A\Leftrightarrow(B\wedge C)$ and (3') is $A\Leftrightarrow C$. At point (3') we know $B$. Every assignment of the propositional variables that satisfies $B$ and (2) also satisfies (3'). In other words, at the position (3') we know
$(A\Leftrightarrow(B\wedge C))\wedge B$
follows semantically. If the propositional proof system of your choice is complete, the above can also be derived using its rules.
The second answer addresses Hoare logic instead of propositional logic. Hoare logic has its own derivations. The neat thing is that most of them can be automated. And they work backwards. In the case at hand, (3') is derived from (4) by copy. After all, at the end of the else clause, the same invariant must hold as after the2018-03-13 19:29:53