 Now consider the existential quantifier “there exists an \(x\) such that \(A\)”. Suppose we add this quantifier to an imperative programming language. What would be its meaning? It would be an instruction to replace the old value of \(x\) by a new value, where the new value has property \(A\). We can decompose this into a part “there exists \(x\)” and a test “\(A\)”. A formula/instruction is a test if the update contributed by it takes the states in the input context one at a time and tests that they satisfy a particular condition. If they do, they are included in the output context; if they don’t, they are discarded. That is, a test is an update that takes an input context and outputs a context that is a subset of the input context. All the formulas of propositional logic in the  Propositional logic as an update logic  section above are tests.