(*
 * Testing of the file ops.  In particular, as of 16nov04, this is just some
 * fiddling to debug the shift-down-one logic in the FileNew postcond.  At some
 * point, this should be the new testing stuff.
 *
 * Finding the bug in the pre-f04 versions of the FileNew postcond was a pretty
 * big deal, and this file sprang from that find.  I believe it was a 205
 * student who pointed it out.  The file.rsl log entry for 5dec04 has further
 * discussion.
 *)

uws.calendars				uws'.calendars

1  2  3  4  5				1  2  3  4  5  6
a  b  c  d  e				   a  b  d  e  f

   uws'.calendars[1] = uc
   uws'.calendars[2] = uws[1]
   uws'.calendars[3] = uws[2]
   uws'.calendars[4] = uws[3]
   uws'.calendars[5] = uws[4]


So here's the kind of test case that we'd run in the new testing regime:

value in_items = [ ... ];
value in_settings = nil;
value in_uid = "gfisher";
value in_cal_name = "Office";
value in_file = nil;
value in_date = nil;
value in_requires_saving = false;

value in_uws = {in_items, ... }

FileNewi(in_uws)?->(out_uws);

OK, it occurs to me quite vividly here that we want to do exactly the same
style of subset testing that we do with code.  I.e., when we have a big
function to test, we write smaller ones that focus on the particular logic we
want to test.  What this means in this case is that we want to focus on the
shift-down logic.  We could give this a try, but let's think a bit more.

Another thing that occurs to me is that we may be able to accomplish a lot of
what we want the new thing for using aux functions.  However, I'm not ready to
abandon the cool thing just yet.  I.e., don't get discouraged just yet, dude.

So, let's try a new sample for the shift-down-one logic, via this aux function:

    function AddAndShiftDownOne(l:Object*, new_thing:Object)->(l':Object*) =
        post:
	    #l' = #l+1;
	        and
	    l'[1] = new_thing
	        and
            forall (i in [1 .. #l])
	        l'[i+1] = l[i];
    end;

AddAndShiftDownOne(['a,'b,'c,'d,'e], 'x)?->['x,'a,'b,'c,'d,'e]

A bit complicated, but not too bad.

Another significant thought is that we want to generate test cases
programmatically in some cases, to avoid the tedium and potential inaccuracy of
hand-built test cases for large, complicated data.  Programmatic data generation
like this should be just fine in FMSL, though it will need to be generated
functionally, unless we want to cheat with the non-fuctional features.