In fpmkunit.pp I found the function FixPath for which I don't understand the exact purpose of. What happens is that if I issue an install command the BaseInstallDir takes the FPCDIR env variable (which is c:\fpc in my case) (line 1472). This value is then passed on to FixPath which converts all '/','\',':' to PathDelim, so I end up with 'c\\fpc' as base install directory.

Two things

1) why is the colon converted to a slash which yields invalid paths (at least on windows)
2) although fpmake initially was developed to be a make tool for FPC, it can (and will be) used for other projects. Therefore I would propose not to initialize FBaseInstallDir with the FPC directory. But rather raise an exception if the basedir is not set in fpmake.pp (when issued an install command only ofcourse). This will make setting this variable mandatory.

Darius

As I mentioned before, assuming some degree of liability for your work is on the horizon.

From
http://www.lightbluetouchpaper.org/2007/08/10/house-of-lords-inquiry-personal-internet-security/

Quote:

"The third area, and this is where the committee has been most far-sighted, and therefore in the short term this may well be their most controversial recommendation, is that they wish to see a software liability regime, viz: that software companies should become responsible for their security failures....

"...in practice it may be a decade or two before there's sufficient case law for vendors to know quite where they stand if they ship a product with a buffer overflow, or a race condition, or just a default password."

This will be a major opportunity to be exploited by a vendor who can design apps which show due diligence via Contract Programming.

James

Op Mon, 13 Aug 2007, schreef JK Smith at Grid-Sky:

Let's first get people of type unsafe languages. Type safety with range checking etc. are a big improvement over type unsafe languages. Yes, Pascal is already the language to use if you are interrested in software correctness.

And perhaps Tom Verhoeff's work will lead to contract programming. But I don't believe it will be a requirement for FPC, as after decades, very few people have an interrest in correctness of their programs. Lastly, pre and post conditions are just another runtime check. Checks can be used to show the existance of bugs, but not their absence.

Daniël

Daniël Mantione wrote

Lastly, pre and post conditions are just another runtime check.

No. If you can prove that the conditions always hold, you don't even need to compile to the program to prove its correctness.

There's a company already doing that:

http://www.praxis-his.com/sparkada/intro.asp

Unfortunately the language is rather limited in terms of dynamic, hard-to-prove constructs like exceptions, pointers or gotos.

For the ones who are interested, according to Lockheed:

- Code quality improved by a factor of 10 over industry norms for DO 178B Level A software.
- Productivity improved by a factor of 4 over previous comparable programs.
- Development costs half of that typical for non safety-critical code.

-- http://www.praxis-his.com/sparkada/pdfs/spark_c130j.pdf

The most interesting sentence is probably the last. Doing it correct right from the start is actually cheaper.

Vinzent.

Please move such discussions to fpc-other.

Op Tue, 14 Aug 2007, schreef Vinzent Hoefler:

This isn't feasible. Read on the internet about the Hoare calculus and how is only feasible to do it for small programs. However, those programs aren't a problem to get correct anyway.

There is no realistic way you can prove that a program like FPC itself is correct.

Daniël

Ok. I'll tell Rod what his company is doing for years now, just ain't possi^Wfeasible. ;)
Of course, you won't have much success with a language like Object Pascal, but I'd suggest reading a bit about SPARK before.

And yes, FPC as it is is unprovable (first through all the language constructs used and second the problem most projects will suffer from: it isn't written with proving it in mind).

OTOH, AFAIK, the correctness of the SPARK Examiner is proven. And those are a little bit more than just a dozen lines of code. Of course, it goes nowhere near a couple of millions of lines of code, but FPC does neither, if you just talk about the compiler. And correctness of stuff like the RTL can be proven independently from the compiler itself.

Vinzent.

I suggest that we introduce a boolean property in TInstaller: FPCProject
by default set to True.

If this is True, BaseInstallDir is initialized with FPCDir. If False, it's set to a sensible value:
/usr
on linux, or
c:\program files\packagename
on Windows.

Michael.

Forgot to say that this is obviously a bug, and should be fixed.

Michael.

As long as they can't prove that Goedel is wrong I don't believe in it :)

Why would you like to initialize BaseInstallDir? It will just increases the chance of installing the files in the wrong place. Consider a tool in a project/FPC (which is placed somewhere higher up the tree). If you don't set the BaseInstall dir it gets placed in c:\program files\whatever, but the base directory should be c:\program files\projectname\whatever (or c:\fpc\whatever resp c:\fpc\utils\whatever). The basedir should probably be set as an env string in any case (whith more complex projects involved) or just hardcoded (for simple ones). Anyway something up to the developer to decide and not to fix in fpmkunit.

Just my 2c

Darius

fpmake is intended in the first place as a way to distribute FPC related packages, just as fpcmake was. Therefore the default behaviour should be to install something as a FPC package: the developer should not be forced to do should 'Just work'

It can be adapted to other things as well, but that is then optional, and can be forced by setting properties such as BaseInstallDir.

Michael.

Maybe we can make a TCustomInstaller and TInstaller where the TInstaller will default to install a FPC package (=units) in the default location so the units work out-of-the-box for fppkg and fpc. The TCustomInstaller can be the base for a complete custom installation of independent projects.

Peter

Well, I've seen it in action. And I don't see the reference to Goedel here. Basically it's predicate logic, which is - according to Goedel - both complete and correct.

Of course, they can't solve the halting problem. But most systems they design are not designed to halt, anyway. ;)

Vinzent.

Op Tue, 14 Aug 2007, schreef Vinzent Hoefler:

Very true. You can't solve the problem of deciding wether two programs are equivalent either, that is simply uncomputable.

You can only that a compiler in such a language performs the *intended* Pascal->Assembler transformation correctly, not that the transformation produces an assembler program with identical functionality as the Pascal program.

Unfortunately the process of designing a transformation from Pascal to assembler that is both efficient and correct is difficult.

So, would it be the end of bugs? would prevent
implementation bugs, not design bugs.

Check the bug repository how mbug reports are due to implementation bugs (internalerror, crash) and how many due to design bugs (incorrect code generation, incompatibility, standard conformance).

Daniël

Daniël Mantione wrote

So, would it be the end of bugs? would prevent implementation bugs, not design bugs.

Precisely. Proving that the program behaves according to the specification doesn't help if the specification is wrong. See Ariane5. Or as we are used say: Shit happens.

Vinzent.

Excellent idea !

Michael.

Am I pushing my luck if I propose a TFPCInstaller for FPC? ;)

Darius

No.

Michael.

There's a company already doing that: http://www.praxis-his.com/sparkada/intro.asp

I've read their book. Cool stuff.

James

Let's first get people of type unsafe languages. Type safety with range

checking etc. are a big improvement over type unsafe languages. Yes, Pascal is already the language to use if you are interrested in software correctness.

And perhaps Tom Verhoeff's work will lead to contract programming. But I

don't believe it will be a requirement for FPC, as after decades, very few people have an interrest in correctness of their programs. Lastly, pre and post conditions are just another runtime check. Checks can be used to show the existance of bugs, but not their absence.

Well, I know programmers who turn off range checking and let exceptions fall through empty exception blocks. They don't work with me on projects. My guess is that this is a business issue that will be decided for programmers, not by programmers. Additionally, it's not an issue of absolutes, but of due diligence. Once the bar is raised on what due diligence means for software developers, they'll accept it because they have to.

Before completely dismissing this issue, I hope you guys will consider merging Tom's qualified work into the trunk at some point.

James

Op Tue, 14 Aug 2007, schreef James Smith:

Before completely dismissing this issue, I hope you guys will consider merging Tom's qualified work into the trunk at some point.

Of course it will be considered. I don't think we are there yet though. First, Tom needs to say he is ready for merging though. Second we need to do some peer review on the code. However, I don't think anyone in the team is again his work.

Daniël

Of course it will be considered. I don't think we are there yet though.

First, Tom needs to say he is ready for merging though. Second we need to do some peer review on the code. However, I don't think anyone in the team is again his work.

Excellent, thanks Daniël.

James

James Smith wrote

Well, I know programmers who turn off range checking and let exceptions fall through empty exception blocks. They don't work with me on projects.

Though it is sometimes the best way of doing. It is sometimes better to check ranges explicitly (where it is needed to do so) rather than to let the compiler set checks everywhere.

mm

Op Tue, 14 Aug 2007, schreef mm:

You almost never ship a binary with range checking, since a range check crash is for a end user generally as usefull as the protection fault that can happen when you disable range checking. The performance penalty of range checking is significant.

Range checking during development greatly reduces the change of range bugs going unnoticed into the final product. Further, for a developer, a range check error is much easier to debug than a crash later in the program because a range error caused data strutures to be overwritten.

Daniël

I totally agree with you (I wrote "sometimes").

For instance, if, in a program, I made use of the following types

   TDigitFrame = array[0..0] of Longword;
   PDigitFrame = ^TDigitFrame;
   TPBigIntFrame = array[0..0] of PBigInt;
   PPBigIntFrame = ^TPBigIntFrame;
   etc.

there would not be much places where I could set {$R+} without having to reset {$R-} almost immediately.

mm

Daniël Mantione wrote

You almost never ship a binary with range checking, since a range check crash is for a end user generally as usefull as the protection fault that can happen when you disable range checking.

Hmm.

grep options Makefile.fpc

options=-CiorR -gl -vbehinw -OG3p3r

Well, "almost".

Vinzent.

mm wrote

there would not be much places where I could set {$R+} without having to reset {$R-} almost immediately. grep \$R *.pas

mdc0lzw.pas: {$IFOPT R+} {$DEFINE OPT_R} {$R-} {$ENDIF} mdc0lzw.pas: {$IFDEF OPT_R} {$UNDEF OPT_R} {$R+} {$ENDIF}

Hmm. Here it is rather the other way around. ;)

Vinzent.