Kontrakt är beteendebeskrivningar av webbtjänster. Vi utformar en teori om kontrakt som formaliserar en kunds kompatibilitet med en tjänst och ett säkert utbyte av en tjänst med en annan tjänst. Användningen av avtal säkerställer statiskt att alla möjliga interaktioner mellan kompatibla kunder och tjänster slutförs på ett framgångsrikt sätt. Den tekniska anordning som ligger till grund för teorin är definitionen av filter, som är uttryckligt tvång som förhindrar vissa möjliga beteenden hos tjänster och därmed gör tjänster kompatibla med olika användningsscenarier. Vi visar att filter kan ses som bevis på ett ljudligt och komplett underleverantörsavdragssystem som samtidigt förfinar och utvidgar Hennessys klassiska axiomatisering av mustprovspreordern. Förhållandet är decidable och beslutalgoritmen erhålls genom en cut-eliminering process som bevisar samstämmigheten av underentreprenad som ett logiskt system. Trots den tekniska utvecklingens rikedom bygger det resulterande tillvägagångssättet på enkla idéer och grundläggande intuitioner. Anmärkningsvärt nog är dess tillämpning mestadels oberoende av det språk som används för att programmera tjänsterna eller kunderna. Vi beskriver också de möjliga praktiska effekterna av ett sådant arbete och perspektiven på framtida forskning som det öppnar.
Studiet av formella kontraktsteorier studeras i REF med CCS-liknande processer som typrepresentation.
A theory of contracts for web services
{'venue': "POPL '08", 'journal': None, 'mag_field_of_study': ['Computer Science']}