59

First, to dispel a possible cognitive dissonance: reasoning about infinite structures is not a problem, we do it all the time. As long as the structure is finitely describable, that's not a problem. Here are a few common types of infinite structures: languages (sets of strings over some alphabet, which may be finite); tree languages (sets of trees over some ...


30

First off, you're absolutely right: you're on to a real concern. Formal verification transfers the problem of confidence in program correctness to the problem of confidence in specification correctness, so it is not a silver bullet. There are several reasons why this process can still be useful, though. Specifications are often simpler than the code ...


26

This is a standard notation for an inference rule. The premises are put above a horizontal line, and the conclusion is put below the line. Thus, it ends up looking like a "fraction", but with one or more logical propositions above the line and a single proposition below the line. If you see a label (e.g., "LET" or "VAR" in your example) next to it, that's ...


24

Can I find a general algorithm to solve the halting problem for some possible program input pairs? Yes, sure. For example you could write an algorithm that returns "Yes, it terminates" for any program which contains neither loops nor recursion and "No, it does not terminate" for any program that contains a while(true) loop that will definitely be reached ...


21

Let us consider the following inductive definition: $\qquad \displaystyle \begin{align*} &\phantom{\Rightarrow} \quad \varepsilon \in \mathcal{T} \\ w \in \mathcal{T} \quad &\Rightarrow \quad aw \in \mathcal{T}\\ aw \in \mathcal{T} \quad &\Rightarrow \quad baw \in \mathcal{T} \end{align*}$ What is $\mathcal{T}$? Clearly, the set of ...


19

D.W.'s answer is great, but I'd like to expand on one point. A specification is not just a reference against which the code is verified. One of the reasons to have a formal specification is to validate it by proving some fundamental properties. Of course, the specification cannot be completely validated — the validation would be as complex as the ...


16

In contrast to what the nay-sayers say, there are many effective techniques for doing this. Bisimulation is one approach. See for example, Gordon's paper on Coinduction and Functional Programming. Another approach is to use operational theories of program equivalence, such as the work of Pitts. A third approach is to verify that both programs satisfy the ...


15

The constructive equivalence of linear-time fixed point formulae (the logic is called $\nu$TL by some) and Buechi automata is given in a paper by Mads Dam from 1992. Fixed Points of Buchi Automata, FST&TCS 1992. See page 4 for the construction of a $\nu$TL formula from a Buechi automaton. The construction of a Buechi automaton from a $\nu$TL formula ...


14

In the preface of his book “Mathematical Discovery, On Understanding, Learning, and Teaching Problems Solving” George Pólya writes: Solving problems is a practical art, like swimming, or skiing, or playing the piano: you can learn it only be imitation and practice. This book cannot offer you a magic key that opens all the doors and solves all the ...


12

Because a CCS process is worth a thousand pixels – and it is easy to see the underlying LTS – here are two processes that simulates each other but are not bisimilar: $$P = ab + a$$ $$Q = ab$$ $\mathcal{R_1}=\{(ab+a, ab), (b, b), (0,b), (0, 0)\}$ is a simulation. $\mathcal{R_2}=\{(ab, ab+a), (b, b), (0,0)\}$ is a simulation. $P\ \mathcal R_1\ Q$ and $Q\ \...


12

This is clearly reducible from the Halting Problem. If a machine $M$ does not stop on input $x$ then any final state is "useless". Given an input $M,x$ for the Halting problem, it is easy to construct $M_x$ that halts on every input (thus its final state is not useless) if and only if $M$ halts on $x$. That way you can decide Halting Problem if you can ...


10

To elaborate slightly on the "it's impossible" statements, here's a simple proof sketch. We can model algorithms with output by Turing Machines which halt with their output on their tape. If you want to have machines that can halt by either accepting with output on their tape or rejecting (in which case there's no output) you can easily come up with an ...


10

After reading your question the only way I could see and had enough knowledge to tie the topics together was to give a hi-level set of articles that drill down from software verification ending up with trying to unite model checking and theorem proving. Hopefully my comment did that: Take a look at Software verification then Formal verification then Model ...


10

The intuitive answer is that if you don't have unbounded loops and you don't have recursion and you don't have goto, your programs terminate. This isn't quite true, there are other ways to sneak non-termination in, but it's good enough for most practical cases. Of course the converse is wrong, there are languages with these constructs that do not allow non-...


10

Even if there's a simulation in each direction, the simulations back and forth may not relate the same sets of states. Sometimes you have a simulation $R_1$ in one direction, and a simulation $R_2$ in the other direction, and two states $p_1$ and $q$ which are related by $R_1$ but not by $R_2$ nor by any other simulation in the same direction. The canonical ...


10

The state can change in subsequent reduction steps because on the right hand side of $$ \langle while\ B\ do\ S, \sigma \rangle \quad\rightarrow\quad \langle if\ B\ then\ ( {\color{red}{S}};\ while\ B\ do\ S )\ else\ skip, \sigma\rangle $$ the $while$-loop is guarded (preceeded) by $S$. The computation of $S$ may change the state so that the ...


10

In programming language semantics, the notion of program state is not a vague philosophical notion, but a very precise mathematical one. A state $s$ in this small-step operational semantics is a partial function $$ s : \mathbf{Var} \hookrightarrow \mathbb{Z} $$ that records the values of the variables. So if $s\, x = v$, then variable $x$ has value $v$. ...


9

First order logic is undecidable, so SAT solving does not really help. That said, techniques exist for bounded model checking of first order formulas. This means that only a fixed number of objects can be considered when trying to determine whether the formula is true or false. Clearly, this is not complete, but if a counter-example is found, then it truly ...


9

The state $\sigma$ does not change when we consider $B$ to decide whether to perform one iteration of the loop, but it can change later when we run the body $S$. And so, the next time we consider $B$, there can be a change of $\sigma$.


9

Infinite-state system verification is indeed a rather broad topic. First of all, all computers used nowadays can only have a finite number of states, as the amount of RAM is fixed. But that's is mainly a matter of terminology -- any verification technique that needs to iterate over all possible states is doomed from the beginning due to computation time. ...


8

John Harrison's book is an exception in going all the way from theory to practice and making all the source code available. I think you will find it difficult to find an equivalent book for model checking, but there are a few that achieve a close approximation. Principles of Model Checking by Baier and Katoen contains a lot of examples and pretty detailed ...


7

Here is a very informal explanation that might help people unfamiliar with formal notations to get a foot in the door. It does not replace a formal definition! The Ap is the state of your system or your running program. "State" can mean a lot of things but in this case it seems to include a list of all defined local variables and their values. Why is Ap a ...


7

Disclaimer: I'm not sure how useful any of this is for getting this done practically since you have a program, not a Turing Machine. The Cook-Levin Theorem essentially states that you can translate the execution of a Turing Machine into a boolean formula that is polynomial in the length of the TM's execution such that the formula is satisfiable iff the TM ...


6

Probably the most common fixpoint expressions in model checking are things like $\mu X.A\cup(B\cap\circ X)$ and $\nu X.A\cap(B\cup\circ X)$, where $\circ$ is some flavour of "next state" operator. That is, the least $X$ such that $X = A\cup(B\cap\circ X)$, and the greatest $X$ such that $X = A\cap(B\cup\circ X)$, respectively. More generally, we are talking ...


5

I really think "formal" methods are not a very good idea for educational purposes. For that matter, programming a computer is a "formal" method. Does it succeed as an educational tool? What is needed is understanding, intuition, and the ability to deal with abstraction. Formal methods hinder all that. Rather, they promote trial and error, hacking, ...


5

An initial algebra is an initial object in the category of $F$-algebras for a given endofunctor $F : \mathcal{C} \rightarrow \mathcal{C}$. This construction is widely used to gives semantics to data-structures in (functional) programming languages. Intuitively, the functor $F$ captures the "shape" of the data-structure (e.g., $F(X) = 1 + A \times X$, with $...


5

Java Bytecode Similar to Microsoft's CLS, the Java Bytecode that the Java virtual machine executes gives you the (theoretical) possibility of using libraries from one JVM-targeting language with another JVM-targeting language. For example, Java libraries can be used in Scala, which IMO is a much better language than Java itself. Libraries written in Scala ...


5

Partial correctness does not mean that not all statements of a specification are met by an algorithm. Have a look at the Wikipedia article about correctness: Partial correctness of an algorithm means that it returns the correct answer if it terminates. Total correctness means that is it additionally guaranteed that the algorithm terminates. Such a proof ...


5

The first step should be count = 0 while (x*2 > x) x = x*2 count++ to find the largest power of 2 that can fit into the variable. Note that doing +1 instead of *2 is not only much slower but also fails for floating point numbers (the gaps between large consecutive floating point numbers are bigger than 1). The above procedure should work for both ...


Only top voted, non community-wiki answers of a minimum length are eligible