Comments on guisim :: québec: Perfect Developer

Hi David ! Thanks for taking the time to reply to...

2010-02-12T12:49:59.028-05:00

Hi David !

Thanks for taking the time to reply to my post.

I think most of my complaints come down to documentation. As a student, it often felt too complex and unintuitive.

Also, in the context of a single course, It's hard to see how PD can help developing highly critical software. Most of the time, it felt like a complete test suite ( Unit and application-level tests ) would do the same job with less of a hassle.

You response is a very interesting read. If I have to develop a highly critical application, I'll consider using PD.

Hi Guisim, I'm sorry you have not found Perfec...

2010-02-12T10:12:08.418-05:00

Hi Guisim, I'm sorry you have not found Perfect Developer to your liking. We recognise that the documentation could be improved, but we also provide examples and tutorials (see the self-help page on our support site). Regarding your other comments: (1) The not-equals operator is "~=", not "=~". The symbol "~" always means "not" in PD, hence you can also use ~<, ~> and so on. (2) Of course you can declare local names - in fact, you can declare them anywhere in an expression. For example, you can express X to the power 4 as (let X2 ^= X*X; X2*X2). (3) We don't explain the syntax of Perfect in Perfect, it is the library API that we express in Perfect. This is a very natural thing to do - in particular, it shows you all the preconditions. How many API documents do you know that tell you all the preconditions that you must satisfy when calling them? (4) Of course you can create a House class containing a list of inhabitants - although a set would be more appropriate unless you want to impose an ordering on the inhabitants. (5) There are places in PD itself where we can't prove everything is correct, so we have some run-time checks in those places - hence the "illegal branch combination" check that you unfortunately came across. Had you reported this to us (as the message asks you to), we would have supplied you with a patch or workaround. (6) You can control the prover timeouts in the Verification settings tab. You can also tell PD to run the prover at reduced priority. We provide this specifically so that if you are using a single-processor computer, you can carry on editing specifications etc. with good responsiveness. (7) Formal specifications are far from being just a research topic - they have been used for many years in developing highly critical software, such as fly-by-wire aircraft control systems. Would you really want to fly in an aircraft whose critical software was developed using traditional and more error-prone techniques?

J'exige que les arguments de ce texte soient v...

2009-06-22T17:33:44.060-04:00

J'exige que les arguments de ce texte soient validés par un vérificateur de preuve!

:P

C'est l'histoire de mon bacc, des cours où l'on nous montre des choses totalement inutiles. Les profs veulent absolument nous montrer leur sujet d'étude ultra-théorique qui risque fort probablement d'aboutir à... rien.

Y peut ben y avoir du décrochage scolaire. Combien de personnes dans le monde utilisent des outils comme perfect developer régulièrement? 50? Dont 49 sont des profs et l'autre essaye de le hacker? Que dire des automates à pile?

Bref, je trouve que tu as ben raison :)