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