Align language coverage with Java and VDMTools generators

[bandurvp]

For the purpose of a more fair comparison of generators we should endeavour to increase language coverage of VDM2C to approach that of the other two generators. Comparison is more fair this way because the generators can be seen to be equally generic.

[bandurvp]

Constructs to implement for now:

• precondition checks (PJ, VPB)
• map iteration + GC version (PJ)
• Support map iteration in the code-generation platform (PJ)
• map iteration (VPB), signature: TVP vdmMapIterate(TVP map, TVP num)
• map composition + GC version (e.g. {2 |-> 3} comp {1 |-> 2}) (PJ)
• Support map composition in the code-generation platform (PJ)
• map composition (VPB), signature: TVP vdmMapCompose(TVP a, TVP b) to correspond to a comp b in VDM.
• iota (PJ)
• Support iota in the code-generatoin platform (PJ)
• Emit VdmClassHierarchy.h
• Emit NO_INHERITANCE in VdmModelFeatures.h (PVJ)
• nondeterministic statement || (PJ)
• Support the nondeterministic in the code-generation platform (PJ)
• exists1 quantifier (PJ)
• isofbaseclass (VPB), signature: TVP isOfBaseClass(TVP val, int baseID)
• isofbaseclass (PJ)
• Address issue with isofbaseclass in the runtime and enable generator tests, see Align language coverage with Java and VDMTools generators #108 (comment)
• isofclass + GC version (VPB), signature: TVP isOfClass(TVP val, int classID)
• isofclass + GC version (PJ)
• Address issue with isofclass in the runtime and enable generator tests, see Align language coverage with Java and VDMTools generators #108 (comment)
• samebaseclass + GC version (VPB), signature: TVP sameBaseClass(TVP a, TVP b)
• samebaseclass + GC version (PJ)
• Address issue with samebaseclass in the runtime and enable generator tests, see Align language coverage with Java and VDMTools generators #108 (comment)
• sameclass + GC version (VPB), signature: TVP sameClass(TVP a, TVP b)
• sameclass + GC version (PJ)
• Address issue with sameclass in the runtime and enable generator tests, see Align language coverage with Java and VDMTools generators #108 (comment)
• Support isofbaseclass, samebaseclass and sameclass in the code-generation platform
• emit NO_IS flag in VdmModelFeatures.h (PJ)
• is_(...) + GC version VPB
• is_(...) + GC version PVJ
• Support is_(...) for union types as explained in Align language coverage with Java and VDMTools generators #108 (comment) (PJ)
• Full support for is_(...) in the code-generation platform (PJ)
• increase is_ coverage for basic types (VPB), generator to emit the following (PJ), plus their GC versions:
  • isNat PJ
  • isNat VPB
  • isNat1 PJ
  • isNat1 VPB
  • isInt PJ
  • isInt VPB
  • isReal PJ
  • isReal VPB
  • isBool VPB
  • isBool PJ
  • isRat PJ
  • isRat VPB
  • isChar PJ
  • isChar VPB
  • isToken PJ
  • isToken VPB

[bandurvp]

Need to include support for answering the inheritance queries isofbaseclass, isofclass, samebaseclass, sameclass. This must take the form of an array of int included in Vdm.h. Assume the inheritance hirarchy (child -> parent) B -> A, C -> A, D -> C. The array would look like the following:

#include "A.h"
#include "B.h"
#include "C.h"
#include "D.h"

int assoc[] = {CLASS_ID_B_ID, CLASS_ID_A_ID, CLASS_ID_C_ID, CLASS_ID_A_ID, CLASS_ID_D_ID, CLASS_ID_C_ID};

If the model contains no inheritance, then the file containing this information will simply contain an empty array:

int assoc[] = {};

This file must be paired with a corresponding flag NO_INHERITANCE in the VdmModelFeatures.h file.

[peterwvj]

Thanks, Victor. Did you really mean Vdm.h? I mean, the array is generated.

[bandurvp]

Good point, sorry about that! Because it's also generated, maybe it should follow the same approach as the VdmModelFeatures.h file. We could name it VdmClassHierarchy.h

[peterwvj]

Yeah sounds good.

[bandurvp]

@peterwvj I have a questiona bout the isSeqOf... and isSetOf... queries I introduced above. Would it not be a better idea to implement generic isSet and isSeq queries in the runtime and have the generator generate the right structure of calls to these plus isInt etc. for model queries such as is_([[[3]]], seq of seq of seq of int)? It would keep the runtime smaller, plus it would allow any kind of nesting in the VDM model, things like as is_([{'c'}], seq of set of char).

[bandurvp]

After discussion, we will implement a static and recursive mechanism in the runtime supporting arbitrary nesting of seq and set for built-in types.

Signature of the function should be is(TVP value, char nested_type[]).

Encoding scheme for nested_type to follow shortly.

[bandurvp]

@peterwvj , let us try to use the following convention for identifying the nested type. A 'q' for seq of, a 't' for set of and a 'z' at the end to signify the end of the nested type. So the query is_(e, seq of set of nat) would result in char nested_char[] = {'q', 't', 'z'}; that is passed to the is function.

[peterwvj]

Sounds good to me, Victor. Shouldn't is also handle basic types (nat, nat1, char, rat, bool int, token, real) which form the base cases of is. I mean, in the above example it looks like the char array is missing the nat type. So assuming that n identifies nat and z terminates the array I would expect:

• seq of set of nat to be encoded as q, t, n, z
• nat to be encoded as n, z
• set of nat to be encoded as t, n, z
• etc.

Is that what you had in mind?

How does this encoding scheme deal with records?

[bandurvp]

Hi Peter, no, what I had in mind is that the inner type would be passed in the inner_type parameter as, in this case, VDM_NAT.

Regarding products, I liked your convention of identifying character followed by number of fields, I'll work a bit with that and maybe we can have another chat once I wrap my head around it entirely.

[bandurvp]

I would like to use a list like the following in the type encoding array. Many of the built-in types are taken from gcc C++ name mangling:

• int: 'i'
• nat: 'j'
• real: 'd'
• bool: 'b'
• char: 'c'
• nat1: 'k'
• rat: 'e'
• token: 't'
• seq of: 'Q'
• seq1 of: 'Z'
• set of: 'T'
• set1 of: 'Y'
• product: 'P'
• record: 'R'
• map: 'M'
• class: 'W'

Each one of these is prepended with a character '0' if the type is optional, or a character '1' if the type is not optional.

I have worked out and tested the following scheme for encoding the type of the expression being queried, and it works well.

• Class type encodes as {opt, 'W', classID}. When this array is generated, the classID can be the CLASS_ID_XXX_ID define corresponding to that class definition.
• Record type encodes as {opt, 'R', recID}. Same idea for the recID as classID above.
• Product types are the more complicated recursive ones. The scheme I'm using is the following:

{opt, 'P', numOfFields, '*', opt1, field1Type, '*', opt2, field2Type, '*', ..., '*', optn, field(numOfFields - 1)Type, '*'}

With this scheme, the runtime function is only needs two parameters: is(TVP e, char type_encoding[]).

• Map types are the same as records, only the numOfFields field is missing, since this is always 2:

{opt, 'M', '*', opt1, field1Type, '*', opt2, field2Type, '*'}

Some examples:

• seq of int: {'1', 'Q', '1', 'i'}
• seq of [int]: {'1', 'Q', '0', 'i'}
• [seq of int]: {'0', 'Q', '1', 'i'}
• seq of seq of int: {'1', 'Q', '1', 'Q', '1', 'i'}
• seq of set of char: {'1', 'Q', '1', 'T', '1', 'c'}
• int * int: {'1', 'P', 2, '*', '1', 'i', '*', '1', 'i', '*'}. Notice that the number of fields is the number 2, not the character '2'.
• int * (int * [char]): {'1', 'P', 2, '*', '1', 'i', '*', '1', 'P', 2, '*', '1', 'i', '*', '0', 'c', '*', '*'}
• (int * char) * int: {'1', 'P', 2, '*', '1', 'P', 2, '*', '1', 'i', '*', '1', 'c', '*', '*', '1', 'i', '*'}
• map int to seq of char: {'1', 'M', '*', '1', 'i', '*', '1', 'Q', '1', 'c', '*'}

[peterwvj]

Sounds good, Victor, thanks!

[bandurvp]

@peterwvj I've added precondition checking support to this issue because we need it to align with VDMT, but also because it seems like a very good idea in light issues found with the generated Continental model.

[bandurvp]

Hi @peterwvj , in working on the assertions issue I realized that we don't support composition and iteration for maps, but VDMT does. I've added these to the list above.

[peterwvj]

@bandurvp I updated the generator to emit the OO operators (isofbaseclass, isofclass, samebaseclass and sameclass), but I've found runtime related problems with all of them that I need your help to address. Since there's quite a lot of stuff going on, I recommend we sit down face-to-face so I can explain you what's up. My work is available in pvj/ovt-254. However, since I build against Overture 2.5.4-SNAPSHOT (a version which is not released) my build environment is slightly complicated, so I don't recommend you merge this branch.

I've set up numerous tests, inspired by the OO operator examples in the LRM that demonstrate all of these issues. Currently, I've commented out these tests since they produce code that either does not compile or generate wrong results when executed.

[bandurvp]

@peterwvj , regarding #108 (comment) , yes it is a typo, I've updated the comment, sorry about that.

[bandurvp]

Hi @peterwvj , let us talk about the OO operator issues above tomorrow, if you have time.

[peterwvj]

Sure, let's talk tomorrow!

[bandurvp]

@peterwvj , regarding union types, could we make use of the following type of equivalence to just emit a combinatorial is query? For example, it seems that is_(v, nat * (bool | char)) would be equivalent to is_(v, nat * bool) or is_(v, nat * char). This would require no extension to the runtime, only execution overhead. I think this would be much better because augmenting TVP with extra type information would result in a huge increse in heap usage.

[peterwvj]

Perhaps that's a better approach yes, but like you say, it could in theory increase the number of is_ calls drastically. I would like to discuss this approach a bit more tomorrow before I start to implement it.

[peterwvj]

@bandurvp It looks like isGC is missing in the header files.

[peterwvj]

I just added isGC to the header file in pv/ovt-254 in order to make the GC tests pass.

[peterwvj]

is* checks are now implemented. Below is an example that demonstrates how to check if a value is of type nat * (bool | char). Also note that the expression being checked is extracted to a temporary variable in case it has side-effects.

VDM:

public isTupPos : () ==> bool
isTupPos () ==
  return is_(mk_(1, 'a'), nat * (bool | char));

Corresponding C:

static  TVP _Z8isTupPosEV(IsTestCLASS this)	{
  TVP isExpSubject_3 = newProductVar(2, newInt(1), newChar('a'));
  char isExpEncoding_3[] = {'1','P',2,'*','1','j','*','1','b','*'};
  char isExpEncoding_4[] = {'1','P',2,'*','1','j','*','1','c','*'};
  TVP ret_22 = vdmOr(is(isExpSubject_3, isExpEncoding_3), is(isExpSubject_3, isExpEncoding_4));
  return ret_22;
}