Source code annotation language

In a computer system comprising a computer, a method of annotating computer program code stored on a computer-readable medium, wherein the computer program code is operable to cause computer execution to perform according to instructions in the computer program code, the method comprising:

• inserting, by the computer, an annotation at a first value having a first value type in the computer program code;
• wherein the annotation comprises a first instance of a keyword, the first instance of the keyword indicating that the first value satisfies all usability properties necessary to allow a first function to rely on the first value, wherein other instances of the keyword identical to the first instance are operable to indicate that other values having different respective value types satisfy all usability properties necessary to allow functions to rely on the respective other values, wherein use of the keyword associates a pre-determined set of usability properties with a value type, and wherein the usability properties depend on the value type.

In a computer system comprising a computer, a method of annotating computer program code stored on a computer-readable medium, the method comprising:

• inserting, by the computer, an annotation having an annotation argument comprising a second value type in the computer program code, wherein the annotation annotates a variable having a first value type;
• wherein the annotation changes the first value type of the variable to the second value type of the annotation argument.

In a computer system comprising a computer, a method of annotating computer-executable program code stored on a computer-readable medium, the method comprising:

• adding, by the computer, an annotation to a pointer in the computer-executable program code, wherein the annotation describes transferring buffer properties from a second pointer to the pointer;
• and
• including a location parameter with the annotation, wherein the location parameter describes a logical buffer pointed to by the pointer.

One or more computer-readable storage media having encoded thereon computer-executable instructions for performing a method of annotating computer program source code, the method comprising:

• inserting, by a computer, an annotation at a first value having a first value type in the computer program source code;
• wherein the annotation comprises a first instance of a keyword, the first instance of the keyword indicating that the first value satisfies all usability properties necessary to allow a first function to rely on the first value, wherein other instances of the keyword identical to the first instance are operable to indicate that other values having different respective value types satisfy all usability properties necessary to allow functions to rely on the respective other values, wherein use of the keyword associates a pre-determined set of usability properties with a value type, and wherein the usability properties depend on the value type.

One or more computer-readable storage media having encoded thereon computer-executable instructions for performing a method of annotating computer program source code stored on a computer-readable medium, the method comprising:

• inserting, by a computer, an annotation having an annotation argument comprising a second value type in the computer program source code, wherein the annotation annotates a variable having a first value type;
• wherein the annotation changes the first value type of the variable to the second value type of the annotation argument.