Skip to content

Instantly share code, notes, and snippets.

View CodeNinja89's full-sized avatar

CodeNinja89

4 followers · 0 following
View GitHub Profile
@CodeNinja89
CodeNinja89 / prioQ.dfy
Created March 5, 2024 13:35
Priority Queue recursive
class Task {
var prio: nat
var next: Task?
ghost var model: set<nat>
ghost var footprint: set<object>
ghost predicate valid()
reads this, footprint
decreases footprint + {this}
@CodeNinja89
CodeNinja89 / LinkedList_insertion.dfy
Created February 22, 2024 10:17
Based on SO answer
class LL { /* linked list nodes */
var elem: int;
var next: LL?; /* may be null */
constructor (x: int)
ensures elem == x && next == null
{
elem, next := x, null;
}
}
@CodeNinja89
CodeNinja89 / LinkedList_insertion.dfy
Created February 21, 2024 12:28
Ongoing struggles with linked list insertion
class Node {
var data: int
var next: Node?
ghost var footprint: seq<Node>
opaque ghost predicate valid()
reads this, footprint
decreases |footprint|
{
@CodeNinja89
CodeNinja89 / gist:e67b38128cd17fa624cdadf3f57fb517
Last active February 20, 2024 11:30
LinkedListInsert_acceptedAnswer.dfy
class Node {
var data: int
var next: Node?
ghost var contents: seq<int>
ghost var footprint: seq<Node>
opaque ghost predicate valid()
reads this, footprint
@CodeNinja89
CodeNinja89 / gist:0361a3c9f8e6661086f28cf733409f4a
Created February 17, 2024 13:26
Working example of Linked List Insertion
class Node {
var data: int
var next: Node?
ghost var contents: seq<int>
ghost var footprint: seq<Node>
opaque ghost predicate valid()
reads this, footprint
@CodeNinja89
CodeNinja89 / LinkedList.dfy
Created February 9, 2024 16:06
Linked List insertion in Dafny
class Node {
var data: int
var next: Node?
ghost var footprint: set<object>
ghost var contents: seq<int>
ghost predicate valid()
reads this, footprint
{
@CodeNinja89
CodeNinja89 / index.html
Last active December 24, 2015 03:59
Twitter Android app using Cordova/PhoneGap inAppBrowser plugin. Uses Codebird-js library to log in (using OAuth authorization) and use Twitter API. Uses callback URL instead of PIN-based authorization.
<!DOCTYPE html>
<html>
<head>
<title>MooTweet</title>
<script type="text/javascript" charset="utf-8" src="js/cordova.js"></script>
<script type="text/javascript" charset="utf-8" src="js/jquery-min.js"></script>
<script type="text/javascript" charset="utf-8" src="js/sha1.js"></script>
<script type="text/javascript" charset="utf-8" src="js/codebird.js"></script>
<script type="text/javascript" charset="utf-8" src="js/some.js"></script>
@CodeNinja89
CodeNinja89 / some.js
Last active December 23, 2015 12:29
Use Codebird-JS library to periodically fetch user's home timeline. The catch: uses Apache Cordova and the app runs on Android. Tested using: Android 4.1.2, Cordova 2.9.0 and Codebird 2.4.3. Uses pin based authentication. Once authenticated, the OAuth access token and token secret are stored in the InAppBrowser's local storage hence there is no …
/* thanks to amwelles / widget.html (https://gist.github.com/amwelles/5776750)
* for the following function.
* simple and elegant.
*/
function parseText(text) {
var link = /(\b(https?|ftp|file):\/\/[-A-Z0-9+&@#\/%?=~_|!:,.;]*[-A-Z0-9+&@#\/%=~_|])/ig;
var user = /@(\w+)/ig;
var hashTags = /#(\w+)/ig;
var desc = "";