comp.lang.ada
 help / color / Atom feed
* My new post on dev.to about SPARK
@ 2020-07-09 14:16 mockturtle
  2020-07-09 15:21 ` Fabien Chouteau
                   ` (6 more replies)
  0 siblings, 7 replies; 14+ messages in thread
From: mockturtle @ 2020-07-09 14:16 UTC (permalink / raw)


Dear.all,
first a bit of disclaimer: this is about a recent post of mine on dev.to
I post this here since I think that maybe someone in this group could be interested.

Recently I wrote a small binary search procedure for a software of mine.  Since I always wanted to start using SPARK, I thought that this could be a nice small problem to start playing around with SPARK.  The post on dev.to is about my experience. 

If you are curious

https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id

Riccardo 

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-09 14:16 My new post on dev.to about SPARK mockturtle
@ 2020-07-09 15:21 ` Fabien Chouteau
  2020-07-09 15:27   ` Fabien Chouteau
  2020-07-09 16:35 ` Jeffrey R. Carter
                   ` (5 subsequent siblings)
  6 siblings, 1 reply; 14+ messages in thread
From: Fabien Chouteau @ 2020-07-09 15:21 UTC (permalink / raw)


> https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id
 
Very nice post Riccardo.

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-09 15:21 ` Fabien Chouteau
@ 2020-07-09 15:27   ` Fabien Chouteau
  0 siblings, 0 replies; 14+ messages in thread
From: Fabien Chouteau @ 2020-07-09 15:27 UTC (permalink / raw)


On Thursday, July 9, 2020 at 5:21:24 PM UTC+2, Fabien Chouteau wrote:
> > https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id
>  
> Very nice post Riccardo.

I shared it on reddit: https://www.reddit.com/r/programming/comments/ho4zzp/proving_the_correctness_of_a_binary_search/

Go upvote :)

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-09 14:16 My new post on dev.to about SPARK mockturtle
  2020-07-09 15:21 ` Fabien Chouteau
@ 2020-07-09 16:35 ` Jeffrey R. Carter
  2020-07-09 20:00 ` Simon Wright
                   ` (4 subsequent siblings)
  6 siblings, 0 replies; 14+ messages in thread
From: Jeffrey R. Carter @ 2020-07-09 16:35 UTC (permalink / raw)


On 7/9/20 4:16 PM, mockturtle wrote:
> 
> Recently I wrote a small binary search procedure for a software of mine.
This is good, but why did you write it from scratch? Why not start with an 
available, reusable binary search? Then you would have a proven, generally 
useful component. This is an interesting pedagogical example, but the actual 
algorithm is too specialized to be of general use.

-- 
Jeff Carter
"Well, a gala day is enough for me. I don't think
I can handle any more."
Duck Soup
93

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-09 14:16 My new post on dev.to about SPARK mockturtle
  2020-07-09 15:21 ` Fabien Chouteau
  2020-07-09 16:35 ` Jeffrey R. Carter
@ 2020-07-09 20:00 ` Simon Wright
  2020-07-10  4:17   ` J-P. Rosen
  2020-07-10  7:42 ` Stéphane Rivière
                   ` (3 subsequent siblings)
  6 siblings, 1 reply; 14+ messages in thread
From: Simon Wright @ 2020-07-09 20:00 UTC (permalink / raw)


mockturtle <[email protected]> writes:

> Recently I wrote a small binary search procedure for a software of
> mine.  Since I always wanted to start using SPARK, I thought that this
> could be a nice small problem to start playing around with SPARK.  The
> post on dev.to is about my experience.
>
> If you are curious
>
> https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id

Interesting!

I thought to have a bit of a play with it, and I found that neither CE
2019 nor CE 2020 will prove as is, including "assertion might fail,
cannot prove Bottom < Top"; but it proves just fine with 
   type Element_Type is new Integer;
or
   subtype Element_Type is Integer;

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-09 20:00 ` Simon Wright
@ 2020-07-10  4:17   ` J-P. Rosen
  2020-07-10  6:04     ` Paul Rubin
  0 siblings, 1 reply; 14+ messages in thread
From: J-P. Rosen @ 2020-07-10  4:17 UTC (permalink / raw)


> mockturtle <[email protected]> writes:
>> https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id
> 
Hmmm.. The following O(N**2) function:
function Is_Sorted (Table : Array_Type) return Boolean
   is (for all L in Table'Range =>
         (for all M in Table'Range =>
            (if L > M then Table (L) > Table (M))))
   with Ghost;

can be changed to a O(N) function:
function Is_Sorted (Table : Array_Type) return Boolean
   is (for all L in Table'First .. Table'Last -1 =>
            Table (L) < Table (L+1))
   with Ghost;


-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-10  4:17   ` J-P. Rosen
@ 2020-07-10  6:04     ` Paul Rubin
  2020-07-10  7:47       ` J-P. Rosen
  0 siblings, 1 reply; 14+ messages in thread
From: Paul Rubin @ 2020-07-10  6:04 UTC (permalink / raw)


"J-P. Rosen" <[email protected]> writes:
> Hmmm.. The following O(N**2) function: ...
> can be changed to a O(N) function:
> function Is_Sorted (Table : Array_Type) return Boolean
>    is (for all L in Table'First .. Table'Last -1 =>
>             Table (L) < Table (L+1))
>    with Ghost;

Should it matter?  The code is never executed.  It's only used as a
specification for the theorem prover.

By the way, Riccardo, thanks for posting that.  It was impressive to see
that an executable-looking spec like that could be proved automatically
with the help of just a few pragmas.  I hadn't posted yet because I
haven't yet had a chance to try building and playing with the program.

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-09 14:16 My new post on dev.to about SPARK mockturtle
                   ` (2 preceding siblings ...)
  2020-07-09 20:00 ` Simon Wright
@ 2020-07-10  7:42 ` Stéphane Rivière
  2020-07-10  9:16 ` Nasser M. Abbasi
                   ` (2 subsequent siblings)
  6 siblings, 0 replies; 14+ messages in thread
From: Stéphane Rivière @ 2020-07-10  7:42 UTC (permalink / raw)


> If you are curious

Many thanks too Riccordo,
Very nice pedagogical spark source
I "liked" it on dev.to

-
Be Seeing You
Number Six

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-10  6:04     ` Paul Rubin
@ 2020-07-10  7:47       ` J-P. Rosen
  0 siblings, 0 replies; 14+ messages in thread
From: J-P. Rosen @ 2020-07-10  7:47 UTC (permalink / raw)


Le 10/07/2020 à 08:04, Paul Rubin a écrit :
> "J-P. Rosen" <[email protected]> writes:
>> Hmmm.. The following O(N**2) function: ...
>> can be changed to a O(N) function:
>> function Is_Sorted (Table : Array_Type) return Boolean
>>    is (for all L in Table'First .. Table'Last -1 =>
>>             Table (L) < Table (L+1))
>>    with Ghost;
> Should it matter?  The code is never executed.  It's only used as a
> specification for the theorem prover.

For Spark, no (although I think that the simpler version is more
understandable). But if you run it through an Ada compiler with
assertions on, then it will make a difference.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-09 14:16 My new post on dev.to about SPARK mockturtle
                   ` (3 preceding siblings ...)
  2020-07-10  7:42 ` Stéphane Rivière
@ 2020-07-10  9:16 ` Nasser M. Abbasi
  2020-07-10  9:20   ` Nasser M. Abbasi
  2020-07-23 10:17   ` mockturtle
  2020-09-03 10:32 ` c+
  2020-09-12  4:30 ` sumde121
  6 siblings, 2 replies; 14+ messages in thread
From: Nasser M. Abbasi @ 2020-07-10  9:16 UTC (permalink / raw)


On 7/9/2020 9:16 AM, mockturtle wrote:
> Dear.all,
> first a bit of disclaimer: this is about a recent post of mine on dev.to
> I post this here since I think that maybe someone in this group could be interested.
> 
> Recently I wrote a small binary search procedure for a software of mine.  Since I always wanted to start using SPARK, I thought that this could be a nice small problem to start playing around with SPARK.  The post on dev.to is about my experience.
> 
> If you are curious
> 
> https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id
> 
> Riccardo
> 

Please change code formating so that background is not black. Hard to
read on the eyes.

"Pure black text on white backgrounds can cause eye strain when
users read the text over an extended period. White has 100% color
brightness, and black has 0% color brightness. Such a disparity in
color brightness creates intense light levels that overstimulate
the eyes when reading text"

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-10  9:16 ` Nasser M. Abbasi
@ 2020-07-10  9:20   ` Nasser M. Abbasi
  2020-07-23 10:17   ` mockturtle
  1 sibling, 0 replies; 14+ messages in thread
From: Nasser M. Abbasi @ 2020-07-10  9:20 UTC (permalink / raw)


On 7/10/2020 4:16 AM, Nasser M. Abbasi wrote:
> On 7/9/2020 9:16 AM, mockturtle wrote:
>> Dear.all,
>> first a bit of disclaimer: this is about a recent post of mine on dev.to
>> I post this here since I think that maybe someone in this group could be interested.
>>
>> Recently I wrote a small binary search procedure for a software of mine.  Since I always wanted to start using SPARK, I thought that this could be a nice small problem to start playing around with SPARK.  The post on dev.to is about my experience.
>>
>> If you are curious
>>
>> https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id
>>
>> Riccardo
>>
> 
> Please change code formating so that background is not black. Hard to
> read on the eyes.
> 

Here is more details

https://ux.stackexchange.com/questions/53264/dark-or-white-color-theme-is-better-for-the-eyes

"However, most studies have shown that dark characters on a light
background are superior to light characters on a dark background
(when the refresh rate is fairly high). "

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-10  9:16 ` Nasser M. Abbasi
  2020-07-10  9:20   ` Nasser M. Abbasi
@ 2020-07-23 10:17   ` mockturtle
  1 sibling, 0 replies; 14+ messages in thread
From: mockturtle @ 2020-07-23 10:17 UTC (permalink / raw)


On Friday, July 10, 2020 at 11:16:48 AM UTC+2, Nasser M. Abbasi wrote:
> On 7/9/2020 9:16 AM, mockturtle wrote: 
> > Dear.all, 
> > first a bit of disclaimer: this is about a recent post of mine on dev.to 
> > I post this here since I think that maybe someone in this group could be interested. 
> > 
> > Recently I wrote a small binary search procedure for a software of mine. Since I always wanted to start using SPARK, I thought that this could be a nice small problem to start playing around with SPARK. The post on dev.to is about my experience. 
> > 
> > If you are curious 
> > 
> > https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id 
> > 
> > Riccardo 
> >
> Please change code formating so that background is not black. Hard to 
> read on the eyes. 
> 
> 

OK, I'll try, but I am afraid it is not possible.  You see, the code is written in markdown between ```ada ... ``` and the rendering is done by dev.to. Maybe there is some hidden option somewhere to control this.  I'll check.

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-09 14:16 My new post on dev.to about SPARK mockturtle
                   ` (4 preceding siblings ...)
  2020-07-10  9:16 ` Nasser M. Abbasi
@ 2020-09-03 10:32 ` c+
  2020-09-12  4:30 ` sumde121
  6 siblings, 0 replies; 14+ messages in thread
From: c+ @ 2020-09-03 10:32 UTC (permalink / raw)


On Thursday, 9 July 2020 19:46:22 UTC+5:30, mockturtle  wrote:
> Dear.all,
> first a bit of disclaimer: this is about a recent post of mine on dev.to
> I post this here since I think that maybe someone in this group could be interested.
> 
> Recently I wrote a small binary search procedure for a software of mine.  Since I always wanted to start using SPARK, I thought that this could be a nice small problem to start playing around with SPARK.  The post on dev.to is about my experience. 
> 
> If you are curious
> 
> https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id
> 
> Riccardo

^ permalink raw reply	[flat|nested] 14+ messages in thread

* Re: My new post on dev.to about SPARK
  2020-07-09 14:16 My new post on dev.to about SPARK mockturtle
                   ` (5 preceding siblings ...)
  2020-09-03 10:32 ` c+
@ 2020-09-12  4:30 ` sumde121
  6 siblings, 0 replies; 14+ messages in thread
From: sumde121 @ 2020-09-12  4:30 UTC (permalink / raw)


On Thursday, 9 July 2020 19:46:22 UTC+5:30, mockturtle  wrote:
> Dear.all,
> first a bit of disclaimer: this is about a recent post of mine on dev.to
> I post this here since I think that maybe someone in this group could be interested.
> 
> Recently I wrote a small binary search procedure for a software of mine.  Since I always wanted to start using SPARK, I thought that this could be a nice small problem to start playing around with SPARK.  The post on dev.to is about my experience. 
> 
> If you are curious
> 
> https://dev.to/pinotattari/proving-the-correctness-of-a-binary-search-procedure-with-spark-ada-34id
> 
> Riccardo

^ permalink raw reply	[flat|nested] 14+ messages in thread

end of thread, back to index

Thread overview: 14+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-07-09 14:16 My new post on dev.to about SPARK mockturtle
2020-07-09 15:21 ` Fabien Chouteau
2020-07-09 15:27   ` Fabien Chouteau
2020-07-09 16:35 ` Jeffrey R. Carter
2020-07-09 20:00 ` Simon Wright
2020-07-10  4:17   ` J-P. Rosen
2020-07-10  6:04     ` Paul Rubin
2020-07-10  7:47       ` J-P. Rosen
2020-07-10  7:42 ` Stéphane Rivière
2020-07-10  9:16 ` Nasser M. Abbasi
2020-07-10  9:20   ` Nasser M. Abbasi
2020-07-23 10:17   ` mockturtle
2020-09-03 10:32 ` c+
2020-09-12  4:30 ` sumde121

comp.lang.ada

Archives are clonable: git clone --mirror https://archive.legitdata.co/comp.lang.ada

Example config snippet for mirrors


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git