Formal specification

[seriously disabled]

If you want to write a formal specification of a program written in C++ or Java, then how can you know the logic of the C++ program you've written?

 

I searched the Internet for books which rigorously teach the subjects of semantics of programming languages and formal specification and I couldn't find any and the three I did find are not rigorous and are quite out of date.

---

Merged post follows:

Consecutive posts merged

I'll phrase my question differently.

 

Let's say I wrote a program in C++. How do I create a formal specification of the program I've written?

 

Two popular specification languages are the Z notation and VDM (Vienna Development Method). So if I wrote my program in C++, does it mean I have to translate the C++ program to Z notation or VDM? But how do I do that?

 

Do I need to know the semantics of C++ in order to do this? I searched the net for books which teach the semantics of C++ but couldn't find any.

Edited October 26, 2009 by Uri
Consecutive posts merged.

[bascule]

Formal spec can mean a lot of things.

 

It almost sounds like you want a C++ model checker:

 

http://www.cprover.org/cbmc/

 

Aside from that, you cannot formally specify C++ programs, because C++ is a quasi-superset of C, and C has "dangerous" semantics.

 

Perhaps if your program used a subset of C++ which involved no pointers and used references exclusively you could formally specify it.

 

Is this for a class?

[seriously disabled]

Formal spec can mean a lot of things.

 

It almost sounds like you want a C++ model checker:

 

http://www.cprover.org/cbmc/

 

Aside from that, you cannot formally specify C++ programs, because C++ is a quasi-superset of C, and C has "dangerous" semantics.

 

But what is a quasi-superset and what is dangerous semantics?

 

Is this for a class?

 

No it's not for a class. It's just something I'm interested knowing.

[bascule]

C++ is not a proper superset of C (in the way Objective C is, for example).

 

There are valid C programs which are not valid C++. For example, in C, you can typedef a struct and give both the same name. This isn't valid C++, since in C++ a struct is just a class with everything public by default.

 

The dangerous semantics of C involve pointers. C has an inherently unsafe memory model. Subtle errors, buffer overruns, miscalculated pointer arithmetic, etc can corrupt your program's memory and lead to nondeterministic behavior.