Has anyone here heard of RESOLVE/C++?

[Lase]

I was just wondering, it is what is taught at my school (to the disdain of many, not really myself) and I know that it's not very widespread, but I thought people out here on the internet might have a take on it.

Basically, RESOLVE/C++ is a hybrid of RESOLVE and C++ that uses a C++ compiler and similar syntax and types. It relies heavily on mathematical models used to describe each operation. The math models are just comments, but they are written in a formal mathematical/logic jargon that can help you if you are tasked with coding something and have no idea what they want you to do.

RESOLVE by itself is still in the R&D phase. It uses mathematical models and loop invariants to describe what programs should do, and they get compiled along with the RESOLVE code. The catch is, your program will not compile unless it does exactly what the math says it should do. This leads to the idea that if you can write in this mathy jargon, you can describe to anyone what operation you'd like done, and whoever implements it has to have it exactly correct for it to ever work.

tl;dr: RESOLVE aims to make programs that only do what they are supposed to, and never anything else. Discuss.

[0xBADFEED]

So basically you have to write the program twice?

[Lase]

Kindasorta. The math definitions basically tell you what the programs should do, where as the actual code will tell it how. Things like loop invariants only tell you initial values and the final values. As to how the innards work is the consequence of the programmer.

[Berengal]

What would e.g. "int div(int a, int b){return a / b;}" look like?

[Rysto]

Wow, now this is interesting to me. This is exactly what I described in the "Perfect Language" thread.

[headprogrammingczar]

The concept of RESOLVE sounds like substituting a fancy compiler for bug-fixing to me. If, in fact, it is actually useful, then it is probably something similar to interfaces in Java, where all it does is enforce a naming convention. Mathematics on computers tends to end up becoming a language all its own, so if you really had this all-singing and all-dancing math-language, why the hell aren't you coding in that? RESOLVE/C++ itself seems useful in that it formalizes certain types of comments, but it isn't any more revolutionary than javadoc.exe.

[0xBADFEED]

How is this different from something like Eiffel that supports design by contract?

[Lase]

What would e.g. "int div(int a, int b){return a / b;}" look like?

Just as it would in C++. Unless you mean math language. In math language it would be something like

Code: Select all

/*
ensures
there exists: a, b, c integer
c = #a / #b
*/


The concept of RESOLVE sounds like substituting a fancy compiler for bug-fixing to me. If, in fact, it is actually useful, then it is probably something similar to interfaces in Java, where all it does is enforce a naming convention. Mathematics on computers tends to end up becoming a language all its own, so if you really had this all-singing and all-dancing math-language, why the hell aren't you coding in that? RESOLVE/C++ itself seems useful in that it formalizes certain types of comments, but it isn't any more revolutionary than javadoc.exe.

The point of the math language is that it is supposed to be universally understood, where as coding nuances and syntax may not be. The programmer might not be the one writing the math spec.

[Berengal]

Just as it would in C++. Unless you mean math language. In math language it would be something like

That doesn't really say much about its behaviour, does it? The same holds for +, -, * and several other arithmetic operators as well.
Except that there's no integer c such that a / 0 = c.

[Lase]

Just as it would in C++. Unless you mean math language. In math language it would be something like

That doesn't really say much about its behaviour, does it? The same holds for +, -, * and several other arithmetic operators as well.
Except that there's no integer c such that a / 0 = c.

Good point, but I also left out part of the contract that states the behavior.

It would say

Code: Select all

/*
requires
#b /= 0

ensures
c = #a / #b
*/

This version also assumes that a, b, and c are all arguments of the function. Most are described with other parameters not defined by the operation header.

Here is an example from a recent assignment, although this is the formal definition for the height of a tree, and less of an operation spec.

Code: Select all

math definition HEIGHT (
            t: tree of Item
        ): integer satisfies
        there exists x: Item, str: string of tree of Item
            (t = compose (x, str)  and
             HEIGHT (t) = 1 + STRING_HEIGHT (str))

    math definition STRING_HEIGHT (
            str: string of tree of Item
        ): integer satisfies
        if str = empty_string
        then STRING_HEIGHT (str) = 0
        else there exists t: tree of Item,
                          rest: string of tree of Item
                 (str = <t> * rest  and
                  STRING_HEIGHT (str) =
                      max (HEIGHT (t), STRING_HEIGHT (rest)))


[stephentyrone]

Am I the only one who would rather just have a clearly written english paragraph explaining the function?

[Lase]

Am I the only one who would rather just have a clearly written english paragraph explaining the function?

No, definitely not. In terms of understanding and level of experience with the math sublanguage, plain English may be the way to go with a description to a person, but if you intend to compile a description, it won't work.

If you're interested, you might want to take a look at this.

http://www.cse.ohio-state.edu/~bronish/public/VerificationPoster.pdf

[Rysto]

Am I the only one who would rather just have a clearly written english paragraph explaining the function?

The goal is not to make the function easier to comprehend by humans. The goal is to have the compiler understand the intent of the function, so that the compiler can check that the function does what you claim it does.

[headprogrammingczar]

The goal is not to make the function easier to comprehend by humans. The goal is to have the compiler understand the intent of the function, so that the compiler can check that the function does what you claim it does.

But it makes you write the function twice! How do you represent "Print an 8 character string starting from a random memory location" with math? Why does the compiler even need to know your intentions? It won't make the code any faster or anything else; all it does is test your ability to write a program in two different languages simultaneously. If the math code is so much easier for the compiler to work with, just compile the damn math code and don't even bother with C++! Finally, functions don't do anything but what you make them do. The problem with "what you claim it does" is that you just wrote another function. That is all you did. Learn to do unit testing and you will see how incredibly useless this is.

[Berengal]

I have to agree that this seems like a poor substitute for testing. In Haskell, for example, I can write tests for my monads that look suspiciously similar to the definition of the monad laws. To see if the standard implementation of the function quotRem was correct, I can test it like:

Code: Select all

prop_quotRem a b =
  let (q, r) = quotRem a b
  in b /= 0 ==> q*b + r == a

ghci> quickCheck prop_quotRem
+++ OK, passed 100 tests.

I've done similar things in java (except it doesn't do random testing quote as easily), and in both languages the tests can be run at build-time automatically...

[Rysto]

But it makes you write the function twice!

That's a feature, not a bug. The redundancy is what allows the compiler to check what you're doing.

Learn to do unit testing and you will see how incredibly useless this is.

This addresses a number of problems that unit testing doesn't have a hope of catching. One of the most important is capturing the interactions between components -- something that unit testing can't do.

Here's an example: a lot of multi-threaded systems impose an ordering on mutexes to prevent deadlocks. It's a programming error to acquire mutexes out of order. Out-of-order bugs can be very difficult to catch, though. You can do it at run time but unless you exercise every possible code path in the entire system you can miss a bug. Unit tests will never catch this kind of bug because they don't test the whole system, only a single component.

In a static system, function foo() has to declare that it acquires mutex #5, and all callers of foo() have to be able to prove that they don't hold any mutexes after #5, which prevents out-of-order bugs.

[stephentyrone]

It uses mathematical models and loop invariants to describe what programs should do, and they get compiled along with the RESOLVE code. The catch is, your program will not compile unless it does exactly what the math says it should do. This leads to the idea that if you can write in this mathy jargon, you can describe to anyone what operation you'd like done, and whoever implements it has to have it exactly correct for it to ever work.

There are tasks for which theorem-proving compilers are incredibly useful. I wish I had had something like this when I re-implemented long integer division for a shipping system library, for example (but for x86 ASM, not C++, of course). I was very confident in the code I wrote, but I still (a) ran over one trillion unit tests and (b) wrote a rigorous mathematical proof (in english) in comments, and handed it to two other assembly programmers with math PhDs to verify.

The trouble is that the compiler can't check whether the program implements it exactly correct. It can only check whether or not it is capable of proving that the program implements it correctly. For simple intro-CS / data-structures assignments, and even purely mathematical algorithmic functions (like my integer divide example), this will work fabulously. For "real world" problems of sufficient size, however, the proof tree will be far to large for the compiler to handle, and then you're stuck. If the compiler can't prove your code correct, it will never work, even if it actually is correct.

I have to agree that this seems like a poor substitute for testing. In Haskell, for example, I can write tests for my monads that look suspiciously similar to the definition of the monad laws. To see if the standard implementation of the function quotRem was correct, I can test it like:

Unit tests also have their failings: 100 tests to "see if the standard implementation of the function quotRem was correct"? Come on, Berengal, you're a smart guy; I'm going to guess you've read the section in which Knuth discusses implementing integer division and points out the existence of one particular edge case that random testing can basically never hope to catch =).

[Berengal]

I actually haven't read Knuth. Please enlighten me. Does this still hold for unbounded integers?

As for testing in Haskell, quickcheck tests properties, which can be properties between different parts of the program if you want to. My "test" wasn't meant as a proper test as much as documenting a property that should hold. If you want comprehensive testing, you're probably going to write some Arbitrary instances and various generators as well, as well as some static, known edge cases. Most of the time though, testing for correctness is done by the typechecker... If it compiles, it's correct. Looking for space leaks is much more common than looking for bugs in Haskell...

[headprogrammingczar]

While all of you are ragging on unit tests, remember that they are not mandatory. RESOLVE compile proofs are. You can still compile without unit testing and you can still go through the code by hand and find edge cases yourself. I can live with mostly working code that suffers from a vanishingly improbable edge case. I refuse to write a second program to tell the compiler that the first program works, then have to go through more bugfixing afterward.

[stephentyrone]

Who's ragging on unit tests? I think most of us are pretty strongly supportive of them. I just want to make clear that one should never, ever confuse "passes unit testing" with "is bug free". Similarly, one should never, ever, confuse "cannot be proved correct by the compiler" with "is buggy code".

Both unit tests and proofs have their place, and neither one is particularly good at doing what the other is good at. Know your problem, and pick the correct solution. Whichever you choose, you better have extensive clearly written natural language comments to back it up.

[ComputerAnalysis]

I think Lase may have explained it wrong. The mathematical models describe what the function is supposed to do. There are a few things that need to be stated.
First the mathematical language is actually much easier to understand than English paragraphs once you get used to it. It's much shorter and easier to write than English, and it's mathematical rigorous and clear. If you're a computer science major you should be exposed to mathematics. Math is an intricate part of computer science and should be a core part of any computer science curriculum. Next it's not like if the math code is wrong the code won't compile. Resolve/C++ files are compiled using a standard C++ compiler. All the special keywords are typedefed and all the math code is placed in comments so they are ignored anyway. However they are working on a special compiler that uses to mathematical models to prove that your code is correct. No amount of testing can prove that code is correct, but imagine a compiler that can prove that all your code works as intended. This feature is well worth writing the mathematical models. On an ending note, @ headprogrammingczar, while you may be OK with partially working code, some of us aren't.

[stephentyrone]

First the mathematical language is actually much easier to understand than English paragraphs once you get used to it. It's much shorter and easier to write than English, and it's mathematical rigorous and clear.

No, it isn't. If you read any paper in a mathematical journal, you'll see that it is not composed entirely of mathematical notation. The vast majority of the body of a good article is in relatively simple English prose, with technical mathematical terms and symbols mixed in. This is for readability. I am a professional mathematician, and I would much rather read a paragraph of english comments than one line of symbolic asserts in an obscure technical language.

However they are working on a special compiler that uses to mathematical models to prove that your code is correct. No amount of testing can prove that code is correct, but imagine a compiler that can prove that all your code works as intended. This feature is well worth writing the mathematical models. On an ending note, @ headprogrammingczar, while you may be OK with partially working code, some of us aren't.

You're still left with the problem that the C++ compiler hasn't been proved correct (and likely never will be, given the complexity of C++). Neither has the runtime, the OS, or the system libraries that the program is sitting on top of. Neither has the physical processor hardware been proven correct, or the caches, memory, busses, etc.

I believe that there is tremendous value in this sort of thing, but that one would do well to target a much simpler language than C++, one for which you have a snowball's chance in hell of proving correctness of the compiler. It should use a minimal section of system and hardware features, such that verifying correctness of those is also possible. And of course you run everything on a simple processor and kernel (probably L4 or similar), on hardware with a minimal processor, no cache, no virtual memory, and the simplest bus you can come up with. It'll be slow as molasses, but you have a chance of proving correctness.

[ComputerAnalysis]

No, it isn't. If you read any paper in a mathematical journal, you'll see that it is not composed entirely of mathematical notation. The vast majority of the body of a good article is in relatively simple English prose, with technical mathematical terms and symbols mixed in. This is for readability. I am a professional mathematician, and I would much rather read a paragraph of english comments than one line of symbolic asserts in an obscure technical language.

We're not talking about full out papers, we're talking about simple preconditions and postcondition clauses. In which case it is MUCH simpler to read a contract that is clear, concise, and unambiguous. Have you ever seen any of these contracts? How can you pass judgment on something that you've never tried to read?

You're still left with the problem that the C++ compiler hasn't been proved correct (and likely never will be, given the complexity of C++). Neither has the runtime, the OS, or the system libraries that the program is sitting on top of. Neither has the physical processor hardware been proven correct, or the caches, memory, busses, etc.

Techniques exist that can prove programs correct. The field of software verification is a prominent one. It's an obvious step to take these techniques and combined them with compiler theory, just as AI was to create smarter optimizing compilers. All you need to do is break down the requirement of procedures into a set of logical conditions that need to be fulfilled, just as in any theorem prover. Theorem provers do exist, Isabelle is a popular example. Nobody invalidates Isabelle because of the OS it runs on or the cache, memory, busses, ect.

[stephentyrone]

Techniques exist that can prove programs correct.

Subject to a correctness assumption about correctness of the compiler, runtime, libraries, OS, and hardware, yes. People who do serious machine theorem proving are very clear about this assumption, and have everything set up in such a way that when failures in the things I listed are found, they are able to quickly re-verify all of their machine proofs on a corrected system.

The field of software verification is a prominent one. It's an obvious step to take these techniques and combined them with compiler theory, just as AI was to create smarter optimizing compilers. All you need to do is break down the requirement of procedures into a set of logical conditions that need to be fulfilled, just as in any theorem prover.

I never said that it is impossible, just that C++ is a spectacularly poor choice of language for which to do it (side effects aren't tightly controlled, strict aliasing isn't the default, many fairly basic syntactic constructs are left "implementation defined" but common idioms depend on specific behavior, there's plenty of global state, templates, etc, etc). Almost any other language would be a better choice. What motivated the choice of C++?

[ComputerAnalysis]

What motivated the choice of C++?

C++ provides the user with a lot of functionality. It was the only language that allowed them to impose a Resolve disciple onto the language. It allowed them to implement all the keywords using typedef, create all the components in the way they wanted, implement clear and swap, and implement a few other weird Resolve features that wouldn't seem natural at first glance. It's also taught in the three introductory courses, so they also wanted to present some exposure to a language and software development. They have also tried to impose the language on Ada as well as one other language which I forget. So Resolve started as a separate entity, it's own sort of language, and then was imposed on other languages.

Also, they're well aware that it would be impossible to prove everything about C++, they realized that pretty early on. Their solution was that you had to limit what you could do to what you could prove, and hence Resolve/C++ was born.

[Trickster]

I don't know if people read this thread anymore, but I teach R/C++ (I have for many years now), and I believe I can illuminate the motivation. Several anal-retentively numbered points follow:

1) The Resolve which they use for research on verification of program correctness is NOT the same R/C++ used for teaching purposes.

2) The R/C++ used for teaching purposes doesn't utilize any sort of program verification. It's really just a set of preprocessor directives that allow us to create one-word reserved name comments for things (to annotate the const-ness of parameters passed by reference). We also use a nested template method to store the data members of each object (in a record called "Rep"), and to perform compile-time pseudo-polymorphic behavior.

3) We do include formal contracts which could be used (in principle) to prove program correctness, but this is not implemented. The inclusion of formal contracts is the only part of the course that has no direct application to real-world programming (at least at present), but CSE students had better be able to read the international language of math, so it's definitely within the bounds of what a computer engineer should need to show competence in.

4) The whole point of storing the data members in a separate object is that we can automatically implement a swap operation to move data around. This allows our collections to work with items that may not have a copy operation written for them, and prevents aliasing errors since pointers no longer need to be passed between objects.

5) The whole point of using nested templates to give us pseudo-polymorphic behavior is that we can illustrate how concrete-to-concrete dependencies can be broken without teaching the students first about pointers and dynamic types.

6) The net result of all this is that students don't need to understand how pointers work until the end of the second core class. This allows us to expose them to sophisticated concepts (such as recursively-defined binary search tree methods, where an algorithm may swap "self" with one of its subtrees) before they have to learn about pointers. Under this framework, the only place a pointer error can occur is inside of a non-layered kernel component (one that has a Rep in it, and uses pointers directly). This speeds up the teaching process considerably.

7) There are two main downsides to this. The lesser of these is that clients using components must instantiate templates by filling in the template partially or fully and extending it as a new class type with empty body. This takes up only a small space, but the templates cause a lot of code bloat and there are some performance issues that arise. The greater of these is the terribly hard-to-read error messages that come from deeply nested templates. These are readable but it takes practice and is non-intuitive. Also, we have to use emacs as a compiler, and for most students, emacs sucks.

We are moving from quarters to semesters starting Summer 2012, and the course is being redesigned in Java. The formal contracts will remain, with annotations taking the place of some of the R/C++ design. This is an inevitability as students should really have access to a language they can become proficient in, with fewer quirks. However, this means that students will need to learn about pointers much sooner, as every reference variable in Java is technically an implicit smart pointer. You can't understand = and == or, "Why does New(parameter) not change where *argument* points to?" if you don't understand how pointers work.

So, you can't have everything. But the change will be good. I helped write one of the transfer functions that simulates the swapping of information between objects so that it would work inside an object itself (which is actually pretty difficult to set up, since only "this" is ever passed by reference, inner classes aside). It will be fun teaching it once I get the opportunity.

Also, I'll be quick to defend the work they have done with the "actual" Resolve, something students have never seen. They're pretty much the only place trying to tackle program proofs. They write a number of good articles that get rejected because the reviewers have no idea what they're talking about in "formal" program verification...they've even had reviewers mistake specs for code. The main reason few people are willing to tackle the problem is that it is very hard, primarily because theorem provers are still pretty crappy. They've made a lot of progress in proving the correctness of small programs, and the paradigm they use for coupling of components ensures that if the components work then the coupled version always will too. But much of what they're still trying to prove are things like unusual mathematical algorithms, etc., things that are difficult for humans and computers alike to intuit.

I used to attend their meetings because it's interesting to see just how far they can push this. Dismissing it as "impossible" due to Godel and the incompleteness of math is silly, since this says nothing about which practical programs can be formally verified. So I'm glad someone is researching the area, even if it's just a small group of pioneers. It's not my field of focus, though, so my knowledge ends here.