Skip to content
Hallway
0:00 / 0:00

#whiley#programspecification#contracts

Introduction to Program Specification

Whiley

81 subscribers • 1 video on Hallway

YouTube
  • Recommended by 1 person: 1 in engineering communities.

Beginner. No background in the topic needed.

3.1K views10 years ago1 recommendation

Computer scienceProgramming languagesFormal methods and verificationComputation and complexity

An introduction to the concepts of program specification, including formal and informal ways to state what a program should do.

This lecture provides a basic introduction to the idea of program specification. That is, specifying using either informal or formal language to state exactly what the program should do.

Why it's here

1 person recommends this

What people say. Recommended as an introduction to program contracts, preconditions, postconditions, and compile-time verification.

u/curtisfin r/ProgrammingLanguages • Recommends

On “Property promises?”

These are often called "contracts". They are typically enabled by one of two type-system features: * Refinement types * Dependent types Whiley is a teaching language that uses Z3 to check function contracts at compile-time. Ada SPARK is another language that checks contracts at compile time. Other languages with dependent types include Idris, F\*, Coq, and Agda. Other languages with refinement types include Liquid Haskell, F\*, and Dafny. There is not a bright line that separates the different approaches. Basically, dependent types allow you to refer to expressions in your type language. So, I can not just have a `ListString`, I can have a `ListString, len(myOtherList)`. Refine…
34View on Reddit