Dear all,
I would like to model the following:
public replace_smaller(int[] A, int c, int d){
if (A[d] < A[c]){
A[c] = A[q]
}
return A;
}
and I would like to prove that the resulting array is just like the code.
So I think I should define the following:
val replace_smaller_def = Define `replace_smaller a b (\a. if (nth (a, p) <
nth (a,q)) then ... else ...`;
However I have no idea how to continue with this since, I have no idea how
to access the array or anything like that.
Can someone give me some advice?
Kind regards,
Jun Jie
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
