- eschaton
- Mar 7, 2007
-
Don't you just hate when you wind up in a store with people who are in a socioeconomic class that is pretty obviously about two levels lower than your own?
|
ok now do this for the whole windows os
easy peasy
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 }
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 }
this is what all programming will be like when HP Hovercraft has his way
|
#
¿
Nov 28, 2017 10:16
|
|
- Adbot
-
ADBOT LOVES YOU
|
|
|
#
¿
May 10, 2024 19:09
|
|
- eschaton
- Mar 7, 2007
-
Don't you just hate when you wind up in a store with people who are in a socioeconomic class that is pretty obviously about two levels lower than your own?
|
i'm going to learn F# i think. does it still require that you declare your functions before using them within the same lexical scope? or was it something weird about file names? i cant remember.
I think people were confused by F# because it uses in-order evaluation, like Lisp or ML or Haskell, rather than a C-like independent/static compilation model
so code within files needs to be ordered and the files themselves need to be ordered as well
|
|
#
¿
Dec 12, 2017 22:34
|
|
- eschaton
- Mar 7, 2007
-
Don't you just hate when you wind up in a store with people who are in a socioeconomic class that is pretty obviously about two levels lower than your own?
|
Is this true of all fp? Like I've mainly done programming in the small type stuff for course work in scheme, sml, and some racket so I haven't had to deal with this, but it sounds hosed up.
e: Possibly less hosed up than having to worry about link order with large C projects though, now that I think about it.
a lot of languages and environments are like this, not just functional ones
the main difference is if what you’re writing is a static description of a system (C, C++, ObjC, Java, C#, Swift) or whether the system is effectively “live” while it’s being compiled (Lisp, Scheme/Racket, Smalltalk, ML, etc.—and JavaScript)
having the system be “live” during compilation can be an advantage, for example you can use its full power at compile time via macros or other forms of metaprogramming
|
|
#
¿
Dec 13, 2017 04:59
|
|
#
¿
Nov 28, 2017 10:16
