proof-of-correctness Questions
1
I am trying to prove that my implementation of Select Sort in Ada is correct. I have tried a few loop invariants, but using gnatprove only proves inner loop's invariant:
package body Selection with...
Hamnet asked 30/3, 2021 at 12:8
1
Solved
I aim to prove that the Horner's Rule is correct. To do so, I compare the value currently calculated by Horner with the value of "real" polynominal.
So I made this piece of code:
package ...
Uriel asked 24/3, 2021 at 18:7
4
Solved
In order to find the diameter of a tree I can take any node from the tree, perform BFS to find a node which is farthest away from it and then perform BFS on that node. The greatest distance from th...
Alnico asked 15/11, 2013 at 20:58
3
Take the following C++14 code snippet:
unsigned int f(unsigned int a, unsigned int b){
if(a>b)return a;
return b;
}
Statement: the function f returns the maximum of its arguments.
Now, th...
Subordinary asked 8/1, 2018 at 13:45
1
Solved
Let's say I have
data Fruit = Apple | Banana | Grape | Orange | Lemon | {- many others -}
and a predicate on that type,
data WineStock : Fruit -> Type where
CanonicalWine : WineStock Grape
...
Hebrew asked 31/1, 2016 at 23:56
1
Solved
Most proof assistants are functional programming languages with dependent types. They can proof programs/algorithms. I'm interested, instead, in proof assistant suitable best for mathematics and on...
Iaverne asked 16/2, 2015 at 9:45
1
Solved
I understand how languages like Coq and Idris can be used to prove properties of programs written in those languages (judging by my little experience in the subject.), but I wonder if there's an ap...
Driggers asked 14/12, 2014 at 14:1
2
Solved
I'm trying to get a fuller picture of the use of the optimal substructure property in dynamic programming, yet I've gone blind on why we have to prove that any optimal solution to the problem conta...
Megacycle asked 27/2, 2014 at 11:44
6
I am trying to compare 2 algorithms. I thought I may try and write a proof for them. (My math sucks, so hence the question.)
Normally in our math lesson last year we would be given a question...
Guardant asked 23/12, 2009 at 10:51
1
Solved
I was thinking about the fact that we can prove a program has bugs. We can test it to assess that it is more or less bug resistant.
But is there a way (even theoretically) to prove that a program ...
Secondguess asked 16/5, 2013 at 10:56
2
Solved
I am new to lambda calculus and struggling to prove the following.
SKK and II are beta equivalent.
where
S = lambda xyz.xz(yz)
K = lambda xy.x
I = lambda x.x
I tried to beta reduce SKK by open...
Isagogics asked 26/4, 2011 at 1:45
1
© 2022 - 2024 — McMap. All rights reserved.