yuyanbao / dafnyr Goto Github PK
View Code? Open in Web Editor NEWDafnyR is an experimental tool for sequential program specification and verification. It is a variant of Dafny and is inspired by region logic. DafnyR preserves most of the features of Dafny Language. DafnyR is built on a fine-grained region logic and allows one to use several styles of specification frame properties in sequential programs: dynamic frames, region logic and separation logic.
License: Other