bedrock.noimport.doc.cpp.class_representations

• Struct & Class
• Tagged Unions
• Untagged Unions

bedrock.noimport.doc.cpp.howto_sequential

• Sequential Specs
  • Range
  • Binary Search Trees
  • EXERCISE: Linked Lists
  • Range Maps

bedrock.noimport.doc.cpp.logic

• |->
• Separation
• Structured Reps
• Magic Wand
• Pure Assertions

bedrock.noimport.doc.cpp.notations

• • State Predicates
  • Representation Predicates
  • Locations

bedrock.noimport.doc.cpp.principles

• Principles