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

DML type checking

 

Hi Hongwi,

Thanks for providing a wealth of information on the DML type system
in your posting.  I was not aware of your work, which I think
is very interesting.

The trick of reducing integer programming assertions to linear
programming assertions is well-known in the program verification
community.  Greg Nelson and Derek Oppen first proposed this idea in
the late 1970's and actually used the simplex method in the VC
simplier in the Stanford Pascal Verifier.  I suspect that the ESC
system (a project initiated by Greg Nelson at DEC/Compaq SRC) uses
this theory among other to prove the verification conditions that
arise in the context of "extended static checking".

>From the perspective of a type system, the simplex method is very
complex.  What do the typing rules look like?  I notice that in your
draft paper "Facilitating Program Verification With Dependent Types",
you state that your dependent type system is intimidatingly complex
and too long to present in a conventional paper.  Doesn't this
statement support my contention that a realisic treatment of array
bounds checking requires an extremely complex type system?

I also wonder if you really implement this theory as a static type
system attached to language syntax.  Do you reject programs that do
not pass your incomplete bounds checker as ill-formed?  I presume that
the answer is yes.  If so, what form of diagnostic do your generate?

Assume that your DML type checker rejects a program because it cannot
confirm a particular loop invariant and the programmer does not know
if the invariant is incorrect or your analysis is too weak to prove
it.  Can the programmer step through some sample executions on test
cases in an attempt to determine if the problem is a bug in the code
or the incompleteness of your type system?  In a soft typing system,
the programmer has this option.  In a static typing system, the
programmer does not.  Do you really prefer the rigid static approach?

If you DML type checking system were configured as a soft
typing system, I would definitely use it.

-- Corky Cartwright

P.S.  You mentioned that you are not aware of any conventional
examples where your checker fails.  I have a simple example that you
may not be able to handle.  Try analyzing the version of quicksort in
the widely used textbook on algorithms by Cormen, Leiserson, and Rivest.  I
will wager that you will need to tweak the program either by peeling
off the first iteration of the loop or adding a ``ghost'' variable to
the code.

P.P.S.  I have two questions about the form of your binary search example.

   {n:nat}
   int bsearch(key: int, vec[n]: int) {
     var: int low, mid, high;
           int x;;

      low = 0; high = arraysize(vec) - 1;

      invariant:
        [i:int, j:int | 0 <= i <= n, 0 <= j+1 <= n] (low: int(i), high: int(j))
      while (low <= high) {
        mid = (low + high) / 2;
        x = vec[mid];
        if (key == x) { return mid; }
        else if (key < x) { high = mid - 1; }
             else { low = mid + 1; }
      }
      return -1;
    }

1.  Why does your binary search example return -1 for a failed search
rather than throwing an exception?  The declared types for the binary
search routine indicate that the key can be any int, but the -1
convention implies that your code does not work correctly for the key
value -1.  Does DML handle exceptions?

2.  Why do you perform two tests in the inner loop rather than one?
Was this merely a stylistic choice or was it dictated by your type system?