Dear all,
thank you for your help and advice. I've modelled it using the functional
version:
val replace_smaller_def = Define `replace_smaller p q = \a : int -> int. if
(a p) < (a q) then (p =+ (a q)) a else a`;
val system_def = Define `system n = {replace_smaller (n-1) 0} UNION
{replace_smaller i (i+1) | i < n-1}`;
So how do I continue? For example I wish to prove that this program does
not increase any value of a[i] for any i < n? I need to have access to both
the state before my program and after my program right? I am not sure how
to express this condition in HOL.
I think somthing with NOT ?e. A[e] > A'[e], where A'[e] is before the
execution... but how can I access this?
Thanks!
2013/4/11 Anthony Fox <[email protected]>
> Just to add to Konrad’s e-mail.
>
> There is a list “write" operation in listTheory — it is defined as follows:
>
> (∀e n. LUPDATE e n [] = []) ∧
> (∀e x l. LUPDATE e 0 (x::l) = e::l) ∧
> ∀e n x l. LUPDATE e (SUC n) (x::l) = x::LUPDATE e n l
>
> Other representation choices include:
>
> - functions of type : ‘a word -> ty
> - partial functions : ‘a word |-> ty
>
> This could make sense if your “int” type is actually a machine word, e.g.
> ``:word32`` in HOL.
>
> Anthony
>
> On 11 Apr 2013, at 18:12, Konrad Slind <[email protected]> wrote:
>
> > Hi J.J. :
> >
> > First you have to choose how arrays are modelled, i.e., which HOL type
> > is going to be used to represent arrays. Choices:
> >
> > - functions of type : num -> ty
> > - finite functions : num |-> ty
> > - lists : ty list
> > - finite products : ty['dim]
> >
> > Summary of the read (A[i]) and write (A[i] := e) operations on array A:
> >
> > A : num -> ty
> > read operation: A i
> > write operation: \j. if (i=j) then e else A j
> > Note: there is already a definition for update in combinTheory,
> using an infix
> >
> > (i =+ e) A = \j. if (i=j) then e else A(j)
> >
> > A : num |-> ty (load finite_mapTheory)
> > read operation: A ' i
> > write : A |+ (i,e)
> >
> > A : ty list
> > read operation: EL i list
> > write operation: not sure an indexed write for lists is defined in
> HOL. If not, the
> > following is one version:
> >
> > update (h::t) 0 e = e::t
> > update (h::t) n e = h::update t (n-1) e;
> >
> > A : ty['dim] (load fcpTheory)
> > read operation: A ' i
> > write operation: (i :+ e) A
> >
> > I hope this helps,
> > Konrad.
> >
> >
> >
> > On Thu, Apr 11, 2013 at 6:10 AM, J. J. W. <[email protected]> wrote:
> > 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
> >
> >
> >
> ------------------------------------------------------------------------------
> > 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
>
>
------------------------------------------------------------------------------
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
