Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] a closer look on std::unique_copy

  • Subject: [Frama-c-discuss] a closer look on std::unique_copy
  • From: moy at adacore.com (Yannick Moy)
  • Date: Sun, 2 Dec 2018 00:37:36 +0100
  • In-reply-to: <5C92CB6F-2421-4C31-824D-0234C9A915CC@fokus.fraunhofer.de>
  • References: <5C92CB6F-2421-4C31-824D-0234C9A915CC@fokus.fraunhofer.de>
Hi Jens,

-- "Gerlach, Jens" (2018-11-15)
> Dear Frama-C users,
>  
> the team of “ACSL by Example” has written a technical report where we look in some detail on various aspects of testing and formal verification
> the algorithm “unique_copy” from the C++ standard library.
> (Of course, for the purpose of verification with Frama-C/WP, we had to look at an re-implementation of this algorithm in C.)
>  
> This report looks in much more detail on the various aspects of a (simple) algorithm than we have usually done within “ACSL by Example”.
> We therefore hope that it provides some useful insights for the Frama-C community.

Thanks for the interesting read.
It's nice to see how such challenges can be addressed with Frama-C.

Of course, that made me curious about how this could be addressed in SPARK, as we have a different approach wrt axiomatization, assertion semantics and ghost code. In particular, you cannot define an axiomatization in SPARK (on purpose, to avoid introducing unsoundness), you cannot use the infinite integer type as liberally in assertions as in ACSL (in general you are constrained to machine integer types), and finally ghost code is executable. So I could not reuse exactly the same approach as you.

Nonetheless, I'm happy to say that I could address the challenge in SPARK as well!
Instead of axiomatizations, I'm using recursive ghost functions to define the UniqueSize and UniquePartition (which became Unique_Size and Unique_Partition in SPARK, to use the most general convention in Ada...) together with suitable preconditions and postconditions on these to both defend against misuse (runtime errors, as these are executable in SPARK) and to prove the necessary properties of these functions by induction. 

I had to define an auxiliary function Size_Segment to be able to define in this way Unique_Partition by recursion (see the code attached), and interestingly my first attempt using the same kind of recursion on Size_Segment failed. I could not find a way to express properties that SMT provers could prove. Instead, I defined an auxiliary function Size_Segment_Aux which also passes during the recursion the starting point of the segment being computed, so that the final segment size is just an arithmetic expression.

I also had to use ghost code to prove intermediate assertions:
- Prove_Size_Segment makes a case distinction in order to prove the final assertion in the procedure. As this procedure has no contract, it is directly inlined where it is called.
- Prove_Unique_Size_Increasing proves by induction that Unique_Size is increasing.
- inside the code of Unique_Copy, the start of the current segment is materialized by a ghost local variable Start

With that, I could prove the following contract on Unique_Copy, which is a direct translation from your paper:

   procedure Unique_Copy
     (A      : Value_Array;
      N      : Size;
      B      : in out Value_Array;
      Copied : out Natural)
   with
     Pre  => N <= A'Length and then A'Length <= B'Length,
     Post => Copied <= N
       and then Copied = Unique_Size (A, N)
       and then (for all K in 1 .. Copied =>
                   B(K) = A (Unique_Partition (A, N, K)))
       and then (for all K in Copied + 1 .. B'Length =>
                   B(K) = B'Old(K));

I'm attaching the code, including a test unit, which can be used to exercise all contracts and ghost code (when you compile it with -gnata switch).
You can reproduce the proofs with SPARK Community 2018, it takes 12 seconds on my laptop (using CVC4 and Z3 as provers, as the third prover Alt-Ergo never needs to be called) using the command-line:

$ gnatprove -P test.gpr --level=2

The one thing which is not proved is the termination of recursive functions. A simple local review (as functions are not mutually recursive) is enough to check that all recursions are well-founded.

I hope others find it interesting!
--
Yannick Moy, Senior Software Engineer, AdaCore

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181202/3f750c32/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: uc.ads
Type: application/octet-stream
Size: 3374 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181202/3f750c32/attachment.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181202/3f750c32/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: uc.adb
Type: application/octet-stream
Size: 3290 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181202/3f750c32/attachment-0001.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181202/3f750c32/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test_uc.adb
Type: application/octet-stream
Size: 906 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181202/3f750c32/attachment-0002.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181202/3f750c32/attachment-0003.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.gpr
Type: application/octet-stream
Size: 26 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181202/3f750c32/attachment-0003.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181202/3f750c32/attachment-0004.html>