Formal specification

Discussion in 'Computer Science & Culture' started by pluto2, Oct 25, 2009.

Thread Status:
Not open for further replies.
  1. pluto2 Valued Senior Member

    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 high-level C++ program you've written?

    I searched the Internet for books which rigorously teach the subjects of the semantics of programming languages and formal specification and I couldn't find any and the ones I did find are not rigorous and are quite out of date.
    Last edited: Oct 25, 2009
  2. Google AdSense Guest Advertisement

    to hide all adverts.
  3. leopold Valued Senior Member

    what are you talking about, flow charting or writing what the program will do?
    the specifications of a program will describe what the program will accomplish, the flow chart will give the logical course of the program.
  4. Google AdSense Guest Advertisement

    to hide all adverts.
  5. pluto2 Valued Senior Member

    Writing what the program will accomplish.
  6. Google AdSense Guest Advertisement

    to hide all adverts.
  7. leopold Valued Senior Member

    the specification is just that, a specification.
    it doesn't deal with the logic of the program itself.

    usually the programmer doesn't write the specification, the person that hires the programmer does that.
    the programmer takes the specification and creates a flow chart depicting how the program will accomplish the specification.
  8. pluto2 Valued Senior Member

    Ok but how does one write such a specification?

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

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

    I searched the net for books which teach the semantics of C++ but couldn't find any.
    Last edited: Oct 26, 2009
  9. leopold Valued Senior Member

    you are asking this question backwards.
    you MUST have the specification BEFORE you write the code.
    even programs "written from your head" have a specification although in this case it isn't on paper.
    the specification describes what the program does, it doesn't matter if the code is C, C++, BASIC, or machine code.
    sample specification:
    i want a program to find all primes between A and B inclusive where A and B is any positive integer.

    you then take this specification and either go straight to coding it or create a flow chart to aid in logical flow of the program.

    after the program is complete you then list all the variables and equations used and what they are for.
    i don't know about any of this.
    wiki has some info on Z notation with some links that might be helpful.
  10. Stryder Keeper of "good" ideas. Valued Senior Member

    From memory of a Course I did some years back, any programming project starts with identify what the project is attempting to do.

    It's then necessary to break it down into a mixture of Pseudocode to step through what the program is going to attempt to do and of course "Documentation". Documentation is important because it helps identify where you are trying to go with the programming, it identifies to other people than just the key programmers what is done and to be done (this means should you have a change in programmers after your first release, you can still get them to pick up where the others left off, otherwise they have to work their way through someone elses code with no clue as to what they were trying to accomplish or what they have already done)

    Flow charts, Diagrams, Storyboards etc are all handy to aid future developers to understand what is/has been achieved.

    Incidentally the reason for mentioning Pseudocode is that the code itself isn't a standard, but just a humanised iteration of what the program does. This can then be read and used to work out what to program in a variety of languages, meaning the documentation can be used for more than one language. Which is extremely handy if you intend cross-platform compatibility.

    On Z Notation here's an example that covers not just the language but a Diagram and State table.

    On VDM

    In the example cases they have an identified objective which is then documented and specified, and then programmed. You will notice that the specification is for a Small portion of an overall program, not an entire program. Namely a specification can be written for a single function like "How to get names and telephone numbers from a MySQL database", not "How the protagonist character can run through a maze and eventually find the end" (The reason for this is because it's best to work with small bitesized chunks rather than a whole program. If you make any errors in your specification at this level, it's easier to correct as a bitesize rather than wade through an entire projects code looking for bugs. Good specifications also help debuggers/code testers to report where errors are.)
  11. dsdsds Valued Senior Member

    Google Software Validation and more specifically, Software Development LifeCycle (SDLC). There are tons of standards and guidances available. some are:

    IEEE_830-1998_Recommended Practice for Software Requirements Specifications
    IEEE_1016-1998_Recommended Practice for Software Design Descriptions
    IEEE1012-1998_Standard for Software Verification and Validation
    GAMP5 - A Risk Based Approach to Compliant GxP Computerized Systems
  12. RubiksMaster Real eyes realize real lies Registered Senior Member

    If you want a Z-specification, then yes, you have to translate it. First you learn Z, then you come up with the predicates, rules, invariants (or whatever your modeling language allows - I've never actually used Z, but I've used Alloy and others).

    Like what, specifically? I might be able to point you to some sources.

    I don't really understand what you're asking. Search also for "formal methods".
Thread Status:
Not open for further replies.

Share This Page