www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Asking for code review - contract programming

reply chopchop <whateveragain222 gmail.com> writes:
Hi guys,

I am working on a personal - and FOSS - project, available here:
https://tinyurl.com/kv62kr7t
(Tiny url => becoz of results ranking on search engines)

The goal is too see if D contract programming features can help 
cover strong design requirements from the aeronautic industry. 
Those requirements are generated from the industry standard 
guideline called DO-178c

#step 1
So I found a github project by three Master students dealing with 
the DO-178, because I actually don't know much about this 
guideline :)
Their project involved to find an idea, write a design document 
following the DO guideline, code the idea, and verify through 
contracts code that the requirements are met.
Their project is using ADA.

#step 2
I wrote the same idea (a snake game) in Dlang, using as much 
contract techniques as I could think of, as a dlang hobbyist, and 
using Adam's lib for terminal. Please not that I did NOT test the 
game on Linux. Windows only. But technically it should work on 
Linux :)

#step 3
This post! I am actually asking the community for code review, to 
have a look at the code and:
- correct any mistake you could find. Propose PR.
- add contract programming features (in/out/do, invariant, 
unittest...) where you think it is necessary. Propose PR.

Important note: I discovered there are 2 levels of contract 
testing.
1. Checking that the code is sound, like verifying func param, etc
2. Ensuring that the game will work as a standard snake game! 
Think win/loose conditions, etc.

I kind of forgot point 2 so far. Feel free to propose PR for 
anything you think could be relevant to a snake game, on top of 
the nitpick.

#step 4 (the interesting part!)
I have already translated the document of the students from 
French to English. This step will involve to compare the 
requirements they chose in their design with the code coverage of 
our reviewed code, which has no external guideline.
Note that I did not check those requirements before starting 
coding my own version of the game. I just followed a rough 
guideline "let's make a game which works and put some contracts 
in it."
It will be interesting to see how much code coverage we can reach 
already.

#step 5
If necessary, fix the missing requirements coverage, and note how 
easy / hard it is to do so.

#step 6
Write a post-mortem document to be added to the repo.


Voilà! I am from the aero industry, and I think it is kind of 
awkward to have those jobs offers in ADA, because they become a 
dead-end for a career.
C/C++ is also used in the industry, but with the same problems 
which lead to the creation of Dlang, somehow. Buffer overflow on 
board a plane is not sexy!

I had been wondering for a while if D could be a part of the 
solution, hence this project. Thanks if you have time to 
contribute.
Jan 07 2022
next sibling parent reply Ali Cehreli <acehreli yahoo.com> writes:
On 1/7/22 06:03, chopchop wrote:


 I am actually asking the community for code review


I've just looked at this.


 - correct any mistake you could find


It looks fine to me. There are a few places that made me think:

In general, adding two Coordinates is suspicious to me:

   https://github.com/Fr3nchK1ss/SnakeD/blob/master/source/coordinate.d#L37

However, subtracting two Coordinates makes sense and should return a 
Distance object.

The following invariant check might be a 'static assert':

   https://github.com/Fr3nchK1ss/SnakeD/blob/master/source/ground.d#L26

(invariant has runtime cost.)

Accounting for the walls with +1, -1, etc. looks scary to me. I wonder 
whether the playground could be detached from the walls and you could 
use the familiar 0 indexed access. Perhaps by slicing inside a bigger 
area or by a special type that hides that logic from us.

A random thought about 'in' and 'out' contract blocks: Instead of adding 
statements inside these blocks, one can use functions to give a name to 
the check and also use the new contract syntax:

   https://github.com/Fr3nchK1ss/SnakeD/blob/master/source/snake.d#L78

So, instead of the following:

     in {
         // The snake shall not backtrack on itself
         assert(body[0] + unitMotion[direction] != body[1]);
     }

Something like this:

   bool updateBody(Direction direction)
   in (!doesBackTrack(direction), "Snake backtracks")
   {
     // The body of the function ...
   }

(Note 'do' is not used with the new syntax.)


 Important note: I discovered there are 2 levels of contract testing.
 1. Checking that the code is sound, like verifying func param, etc


That is also a responsibility of unit testing.


 2. Ensuring that the game will work as a standard snake game! Think
 win/loose conditions, etc.


That part is definitely outside of unit testing and is handled both by 
contract programming and by functional testing.


 I am from the aero industry [...] Buffer overflow on board a plane [...]
 I had been wondering for a while if D could be a part of the solution,
 hence this project.


What do you think? Can the industry guidelines be sufficient to make D 
safe enough? Otherwise, a D program can spend a long time during a GC 
cycle. (So can other languages where destruction of even a single object 
can spend a lot of time but nobody pays attention to that.) Also, the 
program can run out of memory unless run-time dynamic allocation is 
banned by guidelines.

Ali
Jan 11 2022
next sibling parent reply chopchop <yetanethorfake_addr gmail.com> writes:
On Tuesday, 11 January 2022 at 17:40:48 UTC, Ali Cehreli wrote:

 In general, adding two Coordinates is suspicious to me:


You are right, there should be Coordinate and Vector somehow


 Accounting for the walls with +1, -1, etc. looks scary to me. I 
 wonder whether the playground could be detached from the walls 
 and you could use the familiar 0 indexed access. Perhaps by 
 slicing inside a bigger area or by a special type that hides 
 that logic from us.


Yes, that's a bit disturbing at first. I just re-read Ground, in 
fact there is a lack of consistency in the use of those +1, which 
is probably confusing. I will work on it.
But I kept the walls as part of the playground, because indeed 
they are, and the snake can reach "into" the wall. This is of 
course a GameOver condition, but perfectly legit! I realized with 
those "+1" that loosing is part of the game :)
I discovered that the real problem is when the snake tries to 
reach "beyond" the wall, which is then a programming error, and 
there is a contract on that.


use the new contract


I did not know about the new syntax! I am definitely going to use 
it.


 What do you think? Can the industry guidelines be sufficient to 
 make D safe enough? Otherwise, a D program can spend a long 
 time during a GC cycle. (So can other languages where 
 destruction of even a single object can spend a lot of time but 
 nobody pays attention to that.) Also, the program can run out 
 of memory unless run-time dynamic allocation is banned by 
 guidelines.

 Ali


I would say, planes don't do sharp turn :) Maybe small UAVs 
(drones) would be more sensitive to delays. Reliability is more a 
factor. But how much delay are we talking about? More like 1ms, 
10ms, 100ms, 1sec? I mean, if you can give an example of a 
program and its delay, it's interesting.

Then my project has limited focus, GC is another thing. A lot of 
components for aero subsystems are in C, and BetterC retains 
unittesting... and contract if I am not mistaken? Also those 
subsystems have very precise requirements which can most often 
translate into static arrays, etc. There would be so much to 
explore...
Jan 12 2022
parent reply chopchop <stillafakeaddr myaddr.com> writes:
Hello

So I modified the code according to Ali's review. For those 
interested in contracts, it took me a while to find the 
documentation about the new "expression-based" syntax that Ali is 
talking about:

https://dlang.org/changelog/2.081.0.html#expression-based_contract_syntax


Also, the game "kind of" work on Linux, you must:
- download the project file
- cd to SnakeD/
- ```shell
   dub run
   ```
- IMMEDIATELY hit the UP arrow key
- then you can move with the UP DOWN LEFT RIGHT arrow key, but 
there is a bug which is unfortunately outside the scope of my 
project. It seems that on Linux the terminal (arsd lib) is only 
updating when pressing a key. Adam is you read this...
- You can also go to ground.d and update the values of 
playgroundWidth/Height to have a bigger playground, as a 
work-around.

I will let another week pass, if everybody wants to make a review 
/ give some feedback, then I will work on comparing the DO 
requirements to what I obtained with d contract practices.

Then maybe a few updates to the code

Then conclusion

CHeers
Jan 23 2022
parent reply =?UTF-8?Q?Ali_=c3=87ehreli?= <acehreli yahoo.com> writes:
On 1/23/22 07:33, chopchop wrote:


 it took me a while to find the documentation about the new
 "expression-based" syntax that Ali is talking about:

 https://dlang.org/changelog/2.081.0.html#expression-based_contract_syntax


Yeah, coming late to the party, that syntax gets just a brief mention here:

 
http://ddili.org/ders/d.en/contracts.html#ix_contracts.expression-based%20contracts

Ali
Jan 23 2022
parent Vinod K Chandran <kcvinu82 gmail.com> writes:
On Sunday, 23 January 2022 at 15:52:49 UTC, Ali Çehreli wrote:

 On 1/23/22 07:33, chopchop wrote:


There is language called Odin. I just translated the example code 
of 'out' keyword from your book into Odin. See this--
```D
daysInFebruary :: proc(year : int) -> (result : int) {
	defer assert((result == 28 ) || (result == 29), "Only 28 or 29 
is allowed")
	return isLeapYear(year) ? 29 :  28
}
```
Odin using named return values. Defer keyword ensures the 
execution will be occur at the end of the function execution.
Jan 23 2022
prev sibling parent reply Mark <smarksc gmail.com> writes:
On Tuesday, 11 January 2022 at 17:40:48 UTC, Ali Cehreli wrote:

 The following invariant check might be a 'static assert':

   
 https://github.com/Fr3nchK1ss/SnakeD/blob/master/source/ground.d#L26

 (invariant has runtime cost.)

 Ali


Does the compiler not rewrite `assert`s into `static assert`s if 
there is no dependence on runtime values? Maybe this is a 
worthwhile optimization to implement.
Jan 24 2022
parent reply max haughton <maxhaton gmail.com> writes:
On Monday, 24 January 2022 at 12:41:40 UTC, Mark wrote:

 On Tuesday, 11 January 2022 at 17:40:48 UTC, Ali Cehreli wrote:

 The following invariant check might be a 'static assert':

   
 https://github.com/Fr3nchK1ss/SnakeD/blob/master/source/ground.d#L26

 (invariant has runtime cost.)

 Ali


 Does the compiler not rewrite `assert`s into `static assert`s 
 if there is no dependence on runtime values? Maybe this is a 
 worthwhile optimization to implement.


https://d.godbolt.org/z/46q6osKjK The assertions must still 
happen at runtime, however if the compiler can prove (as it does 
with *any* function) that it cannot be called then it will elide 
the assert.
Jan 24 2022
parent chopchop <yetemailfaxe gpmai.com> writes:
Hi guys,

I finished this little project about contract programming. Not 
much, but interesting to do.

This is a link to the github project (tinyed for google 
referencing)

https://tinyurl.com/yc8yvj6n

cheers
Feb 13 2022
prev sibling parent forkit <forkit gmail.com> writes:
On Friday, 7 January 2022 at 14:03:23 UTC, chopchop wrote:

 Hi guys,

 I am working on a personal - and FOSS - project, available here:
 https://tinyurl.com/kv62kr7t
 (Tiny url => becoz of results ranking on search engines)


btw. please.. use full urls.

https://safecomputing.umich.edu/be-aware/phishing-and-suspicious-email/shortened-url-security
Jan 23 2022