Lamport TLA+ Course Lecture 10: Implementation with Refinement Part 1: Preliminaries (HD)

Original Description: A two-part lecture that explains the general meaning of implementation, which involves refinement mappings.

Contents

0:00 - Intro
00:04 - Prologue
00:44 - Recursive Definitions
03:44 - Substitution
09:19 - The AB2 Protocol
14:14 - Checking AB2
16:43 - Liveness of AB2
19:20 - Epilogue