Using array in the contract

[Amirfarhad-Nilizadeh]

Hi,

How should define an array with a primitive type in the "parameterTypes"? I tried to update the type with a different syntax, but it did not work. The contract and the program under test are attached.

I used Randoop version 4.2.6 and Ubuntu 18.4.

java -ea -classpath /home/amirfarhad/Desktop/ProgramAnalysis/codes/Randoop/CopyArray/bin:/home/amirfarhad/Desktop/ProgramAnalysis/Tools/randoop-4.2.6/randoop-all-4.2.6.jar randoop.main.Main gentests --testclass=org.CopyArray --specifications=contract.JSON

Error:
Randoop for Java version "4.2.6, local changes, branch master, commit 5beca45, 2021-05-03".
Error in specifications: Could not load specification operation: {
"classname": "org.CopyArray",
"name": "CopyArray",
"parameterTypes": "[int[], int, int, int[]]"
} while reading file contract.JSON: int[]

CopyArray.zip

[mernst]

The given file contract.JSON is not a valid JSON file and does not conform to the example at https://randoop.github.io/randoop/manual/net_connection_spec.json . So, this looks like a duplicate of #934.

[Amirfarhad-Nilizadeh]

Thank you so much for your time.

[Amirfarhad-Nilizadeh]

Hi,

I hope you are doing well.

I am talking to a Master's student about potential work on translating JML to JSON for Randoop. However, we have a problem writing a contract in JSON to introduce an array with a primitive type (like the earlier CoppyArray attached file that has two array arguments with int type). The following JSON file is valid using this link https://jsonlint.com/.

However, Randoop cannot parse this JSON file. Also, I could not find any example that shows how array types should be defined in Randoop. (Bold part in the following JSON)

[{
"operation": {
"classname": "org.CopyArray",
"name": "CopyArray",
"parameterTypes": [
"int[]", "int", "int", "int[]"
]
},
"identifiers": {
"parameters": [
"b", "iBegin", "iEnd", "a"
]
},
"post": [],
"pre": [{
"guard": {
"description": "the code must be positive",
"condition": "iBegin >= 0"
}
},
{
"guard": {
"description": "the code must be positive",
"condition": "iEnd >= 0"
}
},
{
"guard": {
"description": "iEnd can be larger or equal to iBegin",
"condition": "iEnd >= iBegin"
}

	}
]

}]

Output:

java -ea -classpath /home/amirfarhad/Desktop/ProgramAnalysis/codes/Randoop/CopyArray/bin:/home/amirfarhad/Desktop/ProgramAnalysis/Tools/randoop-4.2.6/randoop-all-4.2.6.jar randoop.main.Main gentests --testclass=org.CopyArray --specifications=contract.JSON
Randoop for Java version "4.2.6, local changes, branch master, commit 5beca45, 2021-05-03".
Error in specifications: Could not load specification operation: {
"classname": "org.CopyArray",
"name": "CopyArray",
"parameterTypes": "[int[], int, int, int[]]"
} while reading file contract.JSON: int[]