Welcome to the most active Linux Forum on the web.
Go Back > Forums > Non-*NIX Forums > Programming
User Name
Programming This forum is for all programming questions.
The question does not have to be directly related to Linux and any language is fair game.


  Search this Thread
Old 06-18-2012, 12:36 PM   #16
Senior Member
Registered: Nov 2005
Distribution: Debian, Arch
Posts: 3,300

Rep: Reputation: 1484Reputation: 1484Reputation: 1484Reputation: 1484Reputation: 1484Reputation: 1484Reputation: 1484Reputation: 1484Reputation: 1484Reputation: 1484

Originally Posted by ph0n3s View Post
That is, We MUST (formally, mathematically) show that a system or subsystem, yes even each and every script, must satisfy it's logical pre-conditions and logical post-conditions, WITHOUT execution (in the case of the verification), and also DURING execution. (the pre-conditions: I was calling sanity-checking-before-operation).
In this case, the sanity-checking-before-operation does not help satisfy the post-conditions, because between the time you check for sanity and the time you actually do the operation, things may change (see TOCTTOU). In other words, the post-condition of sanity-checking is not sanity!

Sanity-checking doesn't help the system satisfy its post-conditions, therefore it doesn't make sense to require it as a pre-condition. It's okay to do sanity-checking to save users' time, but you MUST NOT rely on it for correctness.

EDIT: I read this as saying you're using the sanity-checking for proving correctness, but Nominal Animal reads the opposite. So I guess at least one of us doesn't "see what your sayin"

Last edited by ntubski; 06-18-2012 at 08:32 PM.
Old 06-18-2012, 01:19 PM   #17
Nominal Animal
Senior Member
Registered: Dec 2010
Location: Finland
Distribution: Xubuntu, CentOS, LFS
Posts: 1,723
Blog Entries: 3

Rep: Reputation: 947Reputation: 947Reputation: 947Reputation: 947Reputation: 947Reputation: 947Reputation: 947Reputation: 947
Originally Posted by ph0n3s View Post
An aside , regarding the exception handling, et al:
I do agree. You can see from my shell script suggestion that I prefer to do the pre-checks (like checking if the user exists) too -- I just felt it was important to emphasize one must not think the pre-checks replace run-time checking. The check prevents a doomed attempt, but I do not rely on it: the actual file/directory tests later on will fail gracefully (with the correct logical result) if the user vanishes in the mean time.

(EDIT: Ntubski, you're preaching to the choir. I understood from ph0n3s description that he is not relying on sanity checks before/after for correctness.)

Using pre-checks in an effort to avoid having any kind of error checking during the operation itself is a very prevalent programming technique, and one that really, really irks me. I honestly thought that that was what you were doing, but I guess I was wrong; I apologise. Not only is the technique unreliable (EDIT: as Ntubski mentioned, due to TOCTTOU), because the situation may change at any point, but it also makes it very hard to track the algorithmic restrictions (since they are never tested during the operation). It makes code maintenance much harder in the long-term, and in my experience, always leads to severe bit-rot. The code quality degrades severely over time, as additions and changes are made. The only reason for it, as far as I can see, is pure programmer laziness.

Properly written code that checks for errors is easier to maintain, because you can simply read the code to find out which situations it can and cannot handle. Optimally, the comments should explain the assumptions and requirements for each situation, so later developers get the correct mental picture.

My own coding style is very defensive. (My comments still need a lot of work; I still tend to document what the code does instead of what the intent of the code is. I'm working on it.) For example, when using low-level I/O (which I use a lot, for minimum overhead), I check read() and write() return values for negative values other than -1. They should never occur, and I've felt a bit foolish doing that for years. Recently, a colleague found one case where they do, and it is a kernel bug. (It only occurs with 2.6 series kernels and over 2GB vectored writes on x86-64 using ext4.) The test is essentially free (one if clause per I/O syscall is irrelevant wrt. performance), but I have not seen other code that does that test.

I am not familiar with formal verification methods. I've never worked with software that has required those. Currently I mostly work with molecular dynamics simulations, where the simulation itself may sometimes get unphysical (completely bonkers due to limited precision or invalid starting values, or for other reasons), and it is pretty important for the simulator itself to catch such states. Most computational physicists learn early on to look at the simulation overall to determine if it makes "physical" sense, or is completely unphysical and thus more or less garbage, but sometimes such situations may be disguised or last only for a short time. I find it is much better if the simulation stops, instead of assuming the user catches any errors.

My point is that even if formal verification is too big a hammer for all software in general, programmers should be pragmatic and accept that shit happens way too often, and make sure their software just deals with it the best way it can. Checking if the dung has already hit the fan is not enough; it may happen at any point in time, even if you just checked for it a nanosecond prior. It makes business sense, too. People don't really remember successes that much, but they sure do remember spectacular failures.

Last edited by Nominal Animal; 06-18-2012 at 01:28 PM.


bash scripting, conditionals, permissions

Thread Tools Search this Thread
Search this Thread:

Advanced Search

Posting Rules
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts

BB code is On
Smilies are On
[IMG] code is Off
HTML code is Off

Similar Threads
Thread Thread Starter Forum Replies Last Post
Solution to have svn managed file-permissions and ownership nobody25145147 Linux - Software 0 01-25-2009 07:36 AM
Need permission solution for sharing media among users computercolin Linux - Newbie 2 01-21-2007 11:47 AM
Proposed solution for "status" (aka "problem solved") indicator demerson3 LQ Suggestions & Feedback 12 04-08-2006 02:15 PM
Users Locked Out, Gdm Gone Beserk,14 hours @ work. No Solution yet. fragmented_user Linux - Newbie 17 09-02-2005 06:07 AM
The perfect Solution Windoze users switching to Linux: koolkat Linux - Distributions 1 09-28-2003 12:45 PM > Forums > Non-*NIX Forums > Programming

All times are GMT -5. The time now is 02:01 PM.

Main Menu
Write for LQ is looking for people interested in writing Editorials, Articles, Reviews, and more. If you'd like to contribute content, let us know.
Main Menu
RSS1  Latest Threads
RSS1  LQ News
Twitter: @linuxquestions
Facebook: linuxquestions Google+: linuxquestions
Open Source Consulting | Domain Registration