学术文献库

Consumption of REST services has become a popular means of invoking code provided by third parties, particularly in web applications. Nowadays programmers of web applications can choose TypeScript over JavaScript to benefit from static type checking that enables validating calls to local functions or to those provided by libraries. Errors in calls to REST services, however, can only be found at run-time. In this paper, we present SafeRESTScript (SRS, for short) a language that extends the support of static analysis to calls to REST services, with the ability to statically find common errors such as missing or invalid data in REST calls and misuse of the results from such calls. SafeRESTScript features a syntax similar to JavaScript and is equipped with (i) a rich collection of types (including objects, arrays and refinement types)and (ii) primitives to natively support REST calls that are statically validated against specifications of the corresponding APIs. Specifications are written in HeadREST, a language that also features refinement types and supports the description of semantic aspects of REST APIs in a style reminiscent of Hoare triples. We present SafeRESTScript and its validation system, based on a general-purpose verification tool (Boogie). The evaluation of SafeRESTScript and of the prototype implementations for its validator, available in the form of an Eclipse plugin, is also discussed.