Only want to say

ddcovery antoniocabreraperez at gmail.com
Mon Jan 11 22:12:15 UTC 2021


On Monday, 11 January 2021 at 19:33:26 UTC, kdevel wrote:
> On Monday, 11 January 2021 at 10:14:36 UTC, ddcovery wrote:
>
> [...]
>
>> void zipTo(string srcFolder, string zipFile)
>> in
>> {
>>   assert(srcFolder.exists());
>> }
>> out
>> {
>>   assert(zipPath.exists());
>> }
>> body
>> {
>>   scope (failure)
>>     "Problems generating 7z file".writeln();
>>
>>   ...
>> }
>
> Just my 2 ¢: This is not DbC as I understand it. The conditions
> do not reflect a program state one "can reason about".
It's true.  I suppose you mainly refer to assertions over shared 
(not exclusive) resources: you can't "snapshot" a pre/post state 
and demonstrate that your function is the responsible of this 
transformation.

But the think here is I'm running a set of batch commands (not 
only 7z) over folders/files assuming that no other one is 
interested in.

It is a really relaxed scenery, but enough for the tasks.


> Furthermore
> there is at least one race condition [1] which would be absent 
> if
> the file system operations just fail and throw an exception.
>
> [1] https://en.wikipedia.org/wiki/Time-of-check_to_time-of-use

Absolutelly.  the pre-assert and post-assert are only 
"informative" (documentation) and a development help (I wrote 
assertions before code).  The zip (really a .7z) is performed 
using 7z command execution an response code is checked to raise 
the exception:  important I/O checking is performed as "athomic" 
as possible:

This is the complete method code:

...
void generateZip(string srcPath, string zipPath )
in
{
   assert(srcPath.exists());
}
out
{
   assert(zipPath.exists());
}
body
{
   import std.file : chdir, getcwd;
   import std.path: absolutePath;

   scope (failure)
     "Problems generating 7z file".writeln();

   auto dstPath = zipPath.absolutePath();
   auto actualDir = getcwd();
   scope (exit)
     chdir(actualDir);

   chdir(srcPath);
   format!"7z a %s"(dstPath).exec();
}
...
void exec(string cmd)
{
   import std.process : wait, spawnShell;

   auto result = cmd.spawnShell().wait(); //wait(spawnShell(cmd));
   if (result != 0)
     throw new object.Error(format!"Problems executing command. 
Exit code %d"(result));
}



More information about the Digitalmars-d mailing list