Register a SA Forums Account here!
JOINING THE SA FORUMS WILL REMOVE THIS BIG AD, THE ANNOYING UNDERLINED ADS, AND STUPID INTERSTITIAL ADS!!!

You can: log in, read the tech support FAQ, or request your lost password. This dumb message (and those ads) will appear on every screen until you register! Get rid of this crap by registering your own SA Forums Account and joining roughly 150,000 Goons, for the one-time price of $9.95! We charge money because it costs us money per month for bills, and since we don't believe in showing ads to our users, we try to make the money back through forum registrations.
The Something Awful Forums > Discussion > Serious Hardware/Software Crap > YOSPOS > fp likers: what were you doing the first time you thought fp was good
 
  • Locked thread
Star War Sex Parrot
Oct 2, 2003

atomicthumbs posted:

if your software isn't formally verified, go gently caress yourself
hell yeah check out the sweet invariants I wrote for my hash table
code:
  type hashtbl 'a = {
    mutable size: int ;
    mutable data: data 'a ;
    ghost mutable model: model 'a }

    invariant { length self.data > 0 }
    invariant {
      forall u:key. forall v:'a.
      mem (u, v) self.data[bucket u (length self.data)] <->
      Map.get self.model u = Some v }
    invariant {
      forall u:key. forall v:'a. forall w:'a.
      (mem (u,v) self.data[bucket u (length self.data)] /\
      mem (u,w) self.data[bucket u (length self.data)]) ->
      v = w }
    invariant {
      forall i: int. 0 <= i < length self.data ->
      forall u: key, v: 'a. mem (u,v) self.data[i] ->
      bucket u (length self.data) = i }
proving these during resize was sort of a bitch. this is the signature and contracts for a resize function whose body is like 6 lines
code:
    let rec rehash (new_data : data 'a) (l : bucket 'a) (ghost i : int) : unit =
      requires {
        forall j: int. 0 <= j < new_size ->
        forall u: key, v: 'a. mem (u,v) new_data[j] ->
        bucket u new_size = j }
      requires {
        forall u: key, v: 'a. mem (u,v) l ->
        bucket u old_size = i }
      requires {
        forall u:key. forall v:'a.
        0 <= bucket u old_size < i ->
        (mem (u, v) new_data[bucket u new_size] <->
        Map.get t.model u = Some v) }
      requires {
        forall u:key. forall v:'a.
        bucket u old_size = i ->
        (Map.get t.model u = Some v <-> mem (u, v) l \/
        (mem (u, v) new_data[bucket u new_size])) }
      requires {
        forall u:key. forall v:'a.
        bucket u old_size > i ->
        not (mem (u, v) new_data[bucket u new_size]) }
      requires { new_size = length new_data }
      ensures {
        forall j: int. 0 <= j < new_size ->
        forall u: key, v: 'a. mem (u,v) new_data[j] ->
        bucket u new_size = j }
      ensures {
        forall u:key. forall v:'a.
        0 <= bucket u old_size <= i ->
        (mem (u, v) new_data[bucket u new_size] <->
        Map.get t.model u = Some v) }
      ensures {
        forall u:key. forall v:'a.
        bucket u old_size > i ->
        not (mem (u, v) new_data[bucket u new_size]) }
      variant { l }

* # ¿ Nov 21, 2017 01:37
  • Quote
Adbot
ADBOT LOVES YOU

# ¿ May 10, 2024 14:19
  • Quote
Star War Sex Parrot
Oct 2, 2003

Bloody posted:

idk what any of that means tbh
languages like F* and WhyML allow you to specify contracts with first order logic, and then automated provers can formally verify whether the code actually matches the specification

it's neat I guess but still feels largely academic to me

* # ¿ Nov 21, 2017 22:06
  • Quote
  • Locked thread
The Something Awful Forums > Discussion > Serious Hardware/Software Crap > YOSPOS > fp likers: what were you doing the first time you thought fp was good