Generalize Linear Channels by Usage Annotations

Annotate I’s and O’s with

• Capability (c)“The input/output will succeed (if it is performed)”

• Obligation (o)“The input/output must be performed (though it won’t succeed)”

• "Deadlock" if these assumptions don't hold

Previous slide

Next slide

Back to first slide

View graphic version