| 2 Jul 2020 |
 matthewfl | is there a manual that complete and up to date that specs everything out that I should be looking at, or is it mostly just documentation attached to the various tutorials? | 15:37:42 |
 everett.hildenbrandt | We have the pending documentation here which we add to on an as-asked-for basis: https://github.com/kframework/k/blob/master/pending-documentation.md | 15:45:19 |
| everett.hildenbrandt | So if there is a feature you find is not documented there, you can open an issue and we'll add documentation. | 15:45:35 |
| 5 Jul 2020 |
|  egeas | 09:02:16 |
| 6 Jul 2020 |
 rikard.hjort | I'm having issues getting a proof through with the following causing failure:
#Ceil ( _M [ K <- V ] )
#And
#Ceil ( _M [ K <- V ] [ K ] )
#And
#Not ( {
V
#Equals
_M [ K <- V ] [ K ]
} )
#And
...
I'm trying to force this one through by adding the following, but it's not helping:
rule M:Map [ K - V ] [ K ] = V [simplification]
| 17:09:15 |
| rikard.hjort | Any ideas? | 17:09:19 |
| 7 Jul 2020 |
|  @cerys7003:matrix.org joined the room. | 17:38:52 |
|  sesh | 21:13:58 |
| 8 Jul 2020 |
| @cerys7003:matrix.org left the room. | 00:58:03 |
|  chexxor joined the room. | 19:36:28 |
| chexxor joined the room. | 19:38:27 |
| chexxor | I'm interested in using the K framework project in a future project -- I want to do static analysis of the business logic built on top of a database, composed of multiple languages.
Does this sound like an appropriate application of the K project? | 19:59:52 |
| chexxor | Also, I am guessing that a temporal logic checker, like I hear TLA+ has, would be useful for cross-transaction analysis. Does K Platform do temporal analysis? Or anything like it? | 20:03:41 |
| everett.hildenbrandt | Depends on the type of analysis you want to perform. To be clear, K is not for static analysis, though you can achieve the same results, but K does dynamic (or runtime) analysis/verification. | 20:04:09 |
| chexxor | Is your definition of static analysis basically "what's the cyclomatic complexity of this code"? Or something more general? | 20:05:21 |
| chexxor | I want to do something akin to "type checking" across the languages, which sounds like static analysis to me, a layperson. | 20:06:11 |
| everett.hildenbrandt | Well, my definition of static analysis is the general technique of analyzing code statically, abstracting parts of it, and inferring specific things about the code from that abstracted version. | 20:06:24 |
| everett.hildenbrandt | Type checking can be done statically using abstraction (normal way) or dynamically by executing a program to its type (how we normally approach it in K). | 20:06:56 |
| everett.hildenbrandt | K can do some temporal model checking. It has built-in support for any reachability queries (which encompasses correctness and safety properties) - think of the "All-path Eventually" fragment of most temporal logics. We also have pretty simple/standard ways of encoding temporal properties as reachability queries, but don't have built-in support for them. | 20:11:54 |
| chexxor | Ok, that answers my question for now! It gives me some new things to read and learn, also! Thank you for your help! | 20:19:56 |
|  @rose0525570:matrix.org joined the room. | 23:59:03 |
| 9 Jul 2020 |
|  @demi390600:matrix.org joined the room. | 01:34:18 |
| @demi390600:matrix.org left the room. | 02:33:16 |
| @rose0525570:matrix.org left the room. | 03:52:05 |
|  martina | 20:28:04 |
|  sharma | 20:42:09 |
| 10 Jul 2020 |
|  kermit | 19:24:14 |
| 12 Jul 2020 |
|  hackphobic changed their display name from hackphobia to hackphobic. | 08:30:50 |
| 13 Jul 2020 |
| matthewfl | In the pending documentation, it says "where isPrime(_) is a predicate that can be defined in the usual way." is the way to define new predicates documented? | 16:56:46 |
| everett.hildenbrandt | Well they're just functions defined in sort Bool:
syntax Bool ::= isPrime ( Int ) [function]
rule isPrime(1) => false
rule isPrime(2) => true
... | 17:02:13 |
