viperproject / silver Goto Github PK
View Code? Open in Web Editor NEWDefinition of the Viper intermediate verification language.
License: Mozilla Public License 2.0
Definition of the Viper intermediate verification language.
License: Mozilla Public License 2.0
Pull request ๐ created by bitbucket user Korbinian Breu on 2014-01-18 13:43
Last updated on 2014-01-20 12:59
Original Bitbucket pull request id: 18Participants:
- @mschwerhoff (reviewer)
Source: c9669fa on branch
pw-korbinian-breu/sil_forallfix/default
Destination: 332e7fe on branchmaster
State:
MERGED
Created by @mschwerhoff on 2013-07-30 09:17
Last updated on 2013-11-19 16:57
Type checking the following (probably non-minimal) program
var f: Int
var b: Bool
predicate P(this: Ref) {
acc(this.b, write)
&& (this.b ==> acc(this.f, write))
}
method branch(this: Ref)
requires acc(this.P(), write)
{
assert
(3 > 2)
&& (unfolding acc(this.P(), write)
in (!this.b ? true : true)) // HERE
}
fails with
expected Ref, but got Bool (branch.sil:HERE)
expected Bool, but got Ref (branch.sil:HERE)
Replacing the ite-guard !this.b
with the equivalent (this.b == false)
or with the nonequivalent this.b
makes the program type-check.
Pull request ๐ created by bitbucket user evolutics on 2013-07-03 11:33
Last updated on 2013-07-15 14:06
Original Bitbucket pull request id: 7Participants:
- bitbucket user stefanheule โ๏ธ
Source: unknown commit on branch
default
of an unknown repo
Destination: 2a0bf7a on branchmaster
State:
MERGED
Correction of my own code about transformation of specifications. It now correctly generates statements instead of expressions.
Created by @alexanderjsummers on 2013-09-01 23:48
Last updated on 2014-05-08 13:07
When declaring a field as
var f: int
a requirement failure occurs, with a stack trace (it should be "Int"). It would be better to get a message indicating the probable cause.
Created by @alexanderjsummers on 2013-09-01 23:02
Last updated on 2013-09-01 23:30
(true <==> true) cannot be parsed (at least, as the body of a predicate), whereas (true ==> true) works fine. <==> is the correct symbol for "iff", according to Parser.scala
Pull request ๐ created by bitbucket user evolutics on 2013-05-22 21:35
Last updated on 2013-05-22 22:34
Original Bitbucket pull request id: 4Participants:
- bitbucket user bbrodowsky โ๏ธ
Source: unknown commit on branch
default
of an unknown repo
Destination: ccb3d62 on branchmaster
State:
MERGED
A couple of improved details. Most importantly for the induction part, quantifications over multiple variables are now documented in the SIL grammar.
Created by @mschwerhoff on 2013-11-20 13:14
Last updated on 2014-06-18 17:06
Sequence append can also be applied to sets, as done in this snippet:
method test(x: Set[Int]) returns (y: Set[Int]) {
y := x ++ x
}
As far as I know ++
is not overloaded; union
should be used for sets.
Created by @mschwerhoff on 2013-05-24 15:10
Last updated on 2013-11-19 16:57
The binding power of the dot-operator appears to be wrong.
The snippet
#!text
var Node_n: Ref
method test(this: Ref)
requires this != null && acc(this.Node_n, write)
{
assert this != this.Node_n
}
yields Parse error: Failure: '.' expected but '}' found
.
Replacing the method body with
#!text
var v: Ref := this.Node_n
assert this != v
or simply with
#!text
assert this != this.Node_n
makes the parser happy.
Pull request ๐ created by bitbucket user severinh on 2014-01-07 16:31
Last updated on 2014-01-07 16:58
Original Bitbucket pull request id: 17Participants:
- @mschwerhoff (reviewer) โ๏ธ
Source: df41826 on branch
severinh/sil/default
Destination: 96236a5 on branchmaster
State:
MERGED
Thank you for letting me know about the 'exhaustiveness' compiler warning. There was indeed a bug in a method that did not have a corresponding unit test.
Created by @alexanderjsummers on 2013-09-01 23:59
Last updated on 2014-05-07 14:08
writing acc(root.valid,write)
instead of
acc(root.valid(),write)
causes a class-cast exception (attempting to cast Predicate to Field)
Attachments:
Created by @alexanderjsummers on 2013-09-04 17:14
Last updated on 2014-05-08 12:58
Omitting the receiver for a field access e.g., this.f causes an "Internal error : variable f is not defined". This should be caught by the type-checker/resolver.
Attachments:
Pull request ๐ created by bitbucket user evolutics on 2013-05-03 13:19
Last updated on 2020-01-23 12:28
Original Bitbucket pull request id: 2Participants:
- bitbucket user stefanheule โ๏ธ
- @fpoli โ๏ธ
Source: unknown commit on branch
default
of an unknown repo
Destination: f584241 on branchmaster
Marge commit: 89f6fb4State:
MERGED
Sorry for the duplicate, but I had trouble with access rights on Bitbucket.
The first part is a generalization of the expression transformer to make both pre- and postprocessing of the current expression possible. Moreover, the recursion on the subexpressions depends on a predicate. The partial functions have just Exp
as a codomain instead of Option[Exp]
, since they are partial anyway; correct me if you have something else in mind.
The second part is a function to simplify expressions, which I find useful for automatically generated SIL code. Use it with care. Alternatively, I can keep it in my project if you do not need it here.
Created by @alexanderjsummers on 2013-09-01 23:10
Last updated on 2013-11-19 16:57
(!this.leftDown ==> acc(this.leftValid(),write) )
does not parse, whereas
(this.leftDown ==> acc(this.leftValid(),write) )
does.
I assume this is a bug in the grammar regarding where acc predicates can occur.
(file attached is work in progress)
Attachments:
Created by @alexanderjsummers on 2013-12-12 14:26
Last updated on 2014-05-07 14:45
Leaving an empty parameter list for a predicate definition causes a "head of empty list" exception to be thrown when the predicate is used (inhaled) in an assertion.
Attachments:
Created by @alexanderjsummers on 2013-09-04 10:23
Last updated on 2014-01-22 13:16
Reusing the same quantified variable in the same scope is not supported: it yields an error that the variable is "already defined", the second time.
Attachments:
Created by @alexanderjsummers on 2013-12-11 17:26
Last updated on 2017-11-24 18:11
For a Perm-typed field, it should be possible to use the field value as the second parameter in an acc(.., ..) construct. However, this is rejected.
(this behaviour is seen in test-case all\permissions\epsilons.sil more indirectly, through an unfolding of a predicate, but that case is currently ignored by Silicon).
Attachments:
Created by @mschwerhoff on 2013-05-29 08:54
Last updated on 2013-11-20 13:11
Multiplying permissions with an integer doesn't seen to work. Expressions such as
exhale acc(this.f, 3 * write)
exhale acc(this.f, 3 * epsilon)
result in the error message expected Perm, but got Int
.
Tests can be found in Sil:all/basic/permissions_epsilons.sil
.
Created by @alexanderjsummers on 2013-09-04 18:13
Last updated on 2017-11-26 13:36
When nesting acc(..) inside a quantifier, a requirement failure occurs, saying the body of the quantifier can only occur in positive positions. This is confusing, since this is a positive position, plus it is not the whole body which causes the problem. For example:
requires forall x:Int :: (x + 1 > 4 ==> x > 3) && acc(this.f,write)
(not so obvious that the quantifier spans the conjunction, perhaps)
yields "(x + 1 > 4 ==> x > 3) && acc(this.f,write) can only occur in positive positions".
This is also an exception - it would be better to catch this in the resolver/type-checker
Attachments:
Created by @mschwerhoff on 2013-05-27 14:51
Last updated on 2013-11-19 16:56
The error Parse error: Failure: '{' expected but 'r' found
is thrown for the following snippet taken from the test file Sil:all/basic/while.sil
:
while (j < 3)
invariant r != null
invariant r.f == 2
{
j := j+1
}
The error disappears when the clauses are merged to invariant r != null && r.f == 2
.
Created by @alexanderjsummers on 2013-09-04 13:09
Last updated on 2013-11-20 08:28
x in S ==> x in T
parses as
x in (S ==> (x in T)).
It seems to me that "in" should have stronger precedence than implication.
Pull request ๐ created by @mschwerhoff on 2013-05-17 11:51
Last updated on 2013-05-17 11:52
Original Bitbucket pull request id: 3Source: unknown commit on branch
default
of an unknown repo
Destination: 988f3e8 on branchmaster
Marge commit: eb1f48fState:
MERGED
Pull request ๐ created by bitbucket user severinh on 2013-12-25 12:58
Last updated on 2013-12-25 14:32
Original Bitbucket pull request id: 16Participants:
- @alexanderjsummers โ๏ธ
Source: unknown commit on branch
default
of an unknown repo
Destination: 6ad6563 on branchmaster
State:
MERGED
Created by @alexanderjsummers on 2013-09-01 22:29
Last updated on 2013-11-19 17:02
The attached input file (an attempt to convert Uri's .chalice file) causes a crash when parsing. I don't know whether or not the file in valid SIL. A stack trace is also attached, but it is not very informative (at least, to me)
Attachments:
Created by @mschwerhoff on 2013-06-03 15:29
Last updated on 2014-05-28 12:33
Parsing the Sil program
method test01() {
assert |Seq()| == 0
}
yields an AST in which Seq()
is represented as an EmptySeq
whose typ.elementType
is a TypeVar
.
It appears to be ok to type it as an empty sequence over Ref
or Int
, or any other type for that matter, although it is not really a clean solution.
Created by bitbucket user severinh on 2013-10-29 10:39
Last updated on 2013-11-20 17:17
The parser fails to recognize two consecutive inhale statements if they are not separated by a semicolon.
The type of error depends on whether the inhale expression is wrapped with parentheses:
method foo()
{
inhale (true)
inhale (true) // "hale not defined."
}
method foo()
{
inhale true
inhale true // "Parse error: Failure: `.' expected but `}' found"
}
Using a different keyword for either "inhale" or "in" causes the problem to disappear. But this is obviously not what we want. ;-)
It seems that debugging the parser is rather difficult. Any ideas of what the problem could be?
Created by bitbucket user evolutics on 2013-05-24 17:15
Last updated on 2013-11-20 08:31
The SIL program
#!scala
method variables()
{
var number: Int
var index: Int
number := 1
index := 0 // Line 6
}
cannot be parsed. I receive the parse error Failure: identifier expected
for line 6.
The problem disappears if I replace the variable name index
with another
. Alternatively, terminating line 5 with a semicolon ;
works as well.
Pull request ๐ created by bitbucket user severinh on 2013-12-12 11:26
Last updated on 2013-12-16 14:57
Original Bitbucket pull request id: 15Participants:
- @mschwerhoff โ๏ธ
- bitbucket user severinh
Source: unknown commit on branch
default
of an unknown repo
Destination: e9e3222 on branchmaster
Marge commit: b3bf836State:
MERGED
We would like to reuse SIL's testing infrastructure in Sample, because it is much more sophisticated (based on ScalaTest, supports inline annotations, project-specific annotations, annotations for missing/unexpected output etc.).
This changeset cleanly splits the testing infrastructure into a small SIL-specific part and a generic part that is completely independent from the system under test (e.g. verifier) and the underlying AST.
The new infrastructure uses the term 'output' instead of 'error' for output produced by the system under test. While 'error' makes sense when testing verifiers, 'output' is more generic and can also refer to positive output like inferred invariants. As a result, annotations have been renamed from 'ExpectedError' to 'ExpectedOutput' etc.
Furthermore, the meaning of IDs associated with an output has changed slightly. An output is now associated with a mandatory key ID and an optional value ID. The key ID groups the outputs into namespaces/scopes such as 'precondition.violated' or 'sample.inferred.invariant', while the optional value ID may give additional information such as 'insufficient.permission' or 'n>0', respectively.
The interface of SilSuite has not changed at all. Thus, dependent projects like Silicon do not need to be updated.
There are also a couple of unit tests.
Pull request ๐ created by bitbucket user evolutics on 2013-07-16 14:27
Last updated on 2013-07-21 21:20
Original Bitbucket pull request id: 8Participants:
- bitbucket user evolutics
- bitbucket user stefanheule (reviewer) โ๏ธ
Source: unknown commit on branch
default
of an unknown repo
Destination: bcaf7e7 on branchmaster
State:
MERGED
As decided during the Semper meeting on 6 June 2013, inhale exhale expressions can appear in quantified expressions. This is the third and last point of the corresponding meeting in the archive, which can be found here:
https://bitbucket.org/semperproject/documentation/wiki/Semper%20Meeting%20Archive
For example, it should be possible to have code like ensures forall integer: Int :: [โฆ, โฆ]
, where [โฆ, โฆ]
is an inhale exhale expression.
Moreover, the Kiama library is urgently updated to its latest version 1.5.1. Pretty-printing in earlier versions like 1.5.0 uses too much stack for some programs, causing the stack to overflow. This is now fixed, as documented here: http://wiki.kiama.googlecode.com/hg/doc/1.5.1/notes.html
Pull request ๐ created by bitbucket user severinh on 2013-12-04 12:47
Last updated on 2013-12-04 12:50
Original Bitbucket pull request id: 13Participants:
- @mschwerhoff (reviewer) โ๏ธ
Source: unknown commit on branch
simplify-shallow-copy
of an unknown repo
Destination: 5aa751d on branchmaster
Marge commit: 0b7a0c2State:
MERGED
Thanks for your suggestion Malte. It definitely makes sense.
For some reason, Bitbucket did not allow me to change the branch from which to pull commits, which is why I created a new pull request. The reason why I needed to create a new branch was because my default branch already contains other commits.
Created by @mschwerhoff on 2013-05-29 09:21
Last updated on 2013-11-19 16:57
Consider the following program (take from Sil:all/basic/permissions_epsilons.sil
):
var f: Ref
var p: Perm
method test6(this: Ref)
requires this != null && acc(this.f, 50/100)
ensures acc(this.f, 51/100 + epsilon)
{
exhale acc(this.f, 3 * write)
exhale acc(this.f, 3 * epsilon)
exhale acc(this.f, 2 * epsilon)
inhale acc(this.f, 1/100) /* L1*/
inhale acc(this.f, epsilon + epsilon) /* L2 */
exhale acc(this.f, epsilon) /* L3 */
inhale acc(this.f, epsilon * 5)
}
Parsing it yields Parse error: Failure: '.' expected but 'i' found
reported for line L2
.
Commenting L1
yields Parse error: Failure: '.' expected but 'e' found
reported for line L3
.
Commenting L2
as well finally satisfies the parser.
Strangely, if the program is reduced to (with one of the lines uncommented)
var f: Ref
var p: Perm
method test(this: Ref) {
// inhale acc(this.f, 1/100)
// inhale acc(this.f, epsilon + epsilon)
}
then the parser is satisfied right away. It could thus very well be that the culprit won't be found in L1
or L2
.
Pull request ๐ created by bitbucket user evolutics on 2013-05-03 11:17
Last updated on 2013-05-03 11:58
Original Bitbucket pull request id: 1Participants:
- @mschwerhoff โ๏ธ
- bitbucket user stefanheule โ๏ธ
Source: unknown commit on branch
default
of an unknown repo
Destination: 2a5c5b8 on branchmaster
State:
MERGED
Exp
as a codomain instead of Option[Exp]
, since they are partial anyway; correct me if you have something else in mind.Created by @alexanderjsummers on 2013-09-04 13:05
Last updated on 2013-11-20 08:30
For larger examples, character positions would be extremely useful
Pull request ๐ created by bitbucket user evolutics on 2013-06-05 09:57
Last updated on 2013-06-05 15:10
Original Bitbucket pull request id: 6Source: unknown commit on branch
default
of an unknown repo
Destination: 7c5dac6 on branchmaster
State:
MERGED
This corrects my mistake in the node transformer about indefinite recursions. In the nodes FieldAccess
and PredicateAccess
, the transformer should not recurse on the accessed field and predicate, respectively. If so, this can in turn contain such a node, thereby causing a stack overflow.
Pull request ๐ created by bitbucket user severinh on 2013-11-27 13:26
Last updated on 2013-12-04 12:48
Original Bitbucket pull request id: 12Participants:
- @mschwerhoff (reviewer)
- bitbucket user severinh
Source: unknown commit on branch
default
of an unknown repo
Destination: 5aa751d on branchmaster
State:
DECLINED
There is also a unit test, just in case. ;-)
Created by @mschwerhoff on 2013-07-30 08:52
Last updated on 2013-11-19 16:57
The program
var b: Bool
predicate P(this: Ref) { acc(this.b, write) }
method branch(this: Ref)
requires acc(this.P, write)
{}
makes the parser crash with
java.lang.ClassCastException: semper.sil.ast.Predicate cannot be cast to semper.sil.ast.Field
[info] at semper.sil.parser.Translator.findField(Translator.scala:106)
[info] at semper.sil.parser.Translator.semper$sil$parser$Translator$$exp(Translator.scala:267)
[info] at semper.sil.parser.Translator.semper$sil$parser$Translator$$exp(Translator.scala:316)
[info] at semper.sil.parser.Translator$$anonfun$semper$sil$parser$Translator$$translate$1.apply(Translator.scala:43)
[info] at semper.sil.parser.Translator$$anonfun$semper$sil$parser$Translator$$translate$1.apply(Translator.scala:43)
[info] at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:244)
[info] at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:244)
[info] at scala.collection.immutable.List.foreach(List.scala:318)
[info] at scala.collection.TraversableLike$class.map(TraversableLike.scala:244)
[info] at scala.collection.AbstractTraversable.map(Traversable.scala:105)
[info] ...
If the requires-clause is changed to
requires acc(P(this), write)
then the following parser error is reported:
Parse error: Failure: '.' expected but ',' found
Created by bitbucket user evolutics on 2013-08-09 14:35
Last updated on 2016-02-25 16:58
In the attached program, the SIL type checker does not complain about the types in the axiom takeSuccessorCons
. This axiom is
forall x: Natural, y: Natural, ys: List[A] ::
take(successor(x), cons(y, ys)) == cons(y, take(x, ys))
The type of y
should be the abstract type A
instead of Natural
, since the function cons
has the type (A, List[A]): List[A]
.
Credit goes to Malte for finding this mistake in my axioms!
Attachments:
Created by @mschwerhoff on 2013-11-03 13:26
Last updated on 2014-06-18 17:07
The program
var f: Int
function f(): Bool { true }
method m(x: Ref)
requires acc(x.f, write)
{}
results in the unnecessarily technical error message
expected identifier, but got PFunction(PIdnDef(f),List(),Bool,List(),List(),PBoolLit(true)).
Created by bitbucket user Korbinian Breu on 2014-01-18 13:53
Last updated on 2014-01-20 13:09
Hi,
the following program does not parse correctly, only identifiers seem to be allowed for an assignment to new:
#!scala
var f:Ref
method m(o:Ref)
requires acc(o.f, write)
{
o.f := new()
}
The error is: Parse error: Failure: identifier expected.
Pull request ๐ created by bitbucket user severinh on 2013-11-27 12:37
Last updated on 2013-11-27 12:59
Original Bitbucket pull request id: 11Participants:
- @mschwerhoff โ๏ธ
- bitbucket user severinh
- @alexanderjsummers (reviewer)
Source: unknown commit on branch
default
of an unknown repo
Destination: 886e12f on branchmaster
State:
MERGED
If you prefer, I can move the CFG transformation code to a separate file like CFGTransformer.scala.
Pull request ๐ created by bitbucket user evolutics on 2013-05-25 19:14
Last updated on 2013-05-27 14:48
Original Bitbucket pull request id: 5Source: unknown commit on branch
default
of an unknown repo
Destination: 5689766 on branchmaster
Marge commit: 38264d4State:
MERGED
More transformations I apply when doing the induction translation.
asInstanceOf
seems inevitable here.Hopefully, I am using Scala's generics correctly. Please comment if you know a better way to do all this. Thanks.
Pull request ๐ created by bitbucket user Korbinian Breu on 2013-09-04 15:09
Last updated on 2013-09-04 16:03
Original Bitbucket pull request id: 10Participants:
- @alexanderjsummers โ๏ธ
Source: fa4b3a2 on branch
pw-korbinian-breu/sil/default
Destination: 09b9abe on branchmaster
Marge commit: df3a991State:
MERGED
Created by bitbucket user Korbinian Breu on 2013-09-04 14:21
Last updated on 2013-09-04 18:04
The exception in the title occurs randomly when I run tests with sbt. Is there any workaround to increase this "PermGen" space?
Pull request ๐ created by bitbucket user severinh on 2013-12-05 13:46
Last updated on 2013-12-12 11:14
Original Bitbucket pull request id: 14Participants:
- @mschwerhoff (reviewer) โ๏ธ
- bitbucket user severinh
- @alexanderjsummers (reviewer)
Source: unidentified commit on branch
severinh/sil/generic-test-infrastructure
(Mercurial commit was2a53e4eba176
)
Destination: ebbeffa on branchmaster
State:
DECLINED
We would like to reuse SIL's testing infrastructure in Sample, because it is much more sophisticated (based on ScalaTest, supports inline annotations, project-specific annotations, annotations for missing/unexpected output etc.).
This changeset cleanly splits the testing infrastructure into a small SIL-specific part and a generic part that is completely independent from the system under test (e.g. verifier) and the underlying AST.
The new infrastructure uses the term 'output' instead of 'error' for output produced by the system under test. While 'error' makes sense when testing verifiers, 'output' is more generic and can also refer to positive output like inferred invariants. As a result, annotations have been renamed from 'ExpectedError' to 'ExpectedOutput' etc.
Furthermore, the meaning of IDs associated with an output has changed slightly. An output is now associated with a mandatory key ID and an optional value ID. The key ID groups the outputs into namespaces/scopes such as 'precondition.violated' or 'sample.inferred.invariant', while the optional value ID may give additional information such as 'insufficient.permission' or 'n>0', respectively.
The interface of SilSuite has not changed at all. Thus, dependent projects like Silicon do not need to be updated.
There are also a couple of unit tests.
I'm open for any suggestions for further improvements.
Created by @mschwerhoff on 2013-06-05 15:12
Last updated on 2014-05-07 13:44
The following Sil program passes the type checker, although next
in acc(next.valid, write)
is undefined.
var item: Int
var next: Ref
predicate valid(this: Ref) {
acc(this.item, write)
&& acc(this.next, write)
&& (this.next != null ==> acc(next.valid, write))
}
Created by @alexanderjsummers on 2013-09-04 10:09
Last updated on 2017-03-07 16:46
It's confusing that
var x : Seq[Int] := Seq()
type-checks (because the required type is inferred), but
assert x == Seq()
causes a type-error (which is also currently an exception).
In the latter case, the type needs to be specified manually:
#!scala
assert x == Seq[Int]()
Instead, it would be better to allow the empty sequence to have a polymorphic type, which can match any sequence type.
Attachments:
Created by @alexanderjsummers on 2013-09-04 13:35
Last updated on 2017-11-26 13:24
When typing a conditional expression for which the same exact types have not (yet) been inferred for the two latter operands, a requirement failure occurs (with no useful message). This can easily happen with sequences, because of the lack of type information for empty sequences (as in the example attached).
Attachments:
Created by @alexanderjsummers on 2013-09-01 22:51
Last updated on 2013-11-19 22:13
var value: Int;
causes a parse error, due to the semicolon being unexpected. I think it would be nicer to make the symbol optional, as in Chalice, especially for users unfamiliar with the language.
Created by bitbucket user Korbinian Breu on 2013-11-06 12:56
Last updated on 2013-11-06 13:20
The following piece of code
#!scala
var s:Set[Ref]
predicate inv(this: Ref)
{
!(null in this.s)
}
is not parsed correctly, in seems to have precedence before the dot "."
#!scala
[info] expected Ref, but got Bool (issue.sil:5) (issue.sil:5)
[info] expected one of [Set[.], Multiset[.], Seq[.]], but got Ref (issue.sil:5) (issue.sil:5)
[info] expected Bool, but got Set[Ref] (issue.sil:5) (issue.sil:5) (SilSuite.scala:246)
Created by @mschwerhoff on 2013-07-24 16:42
Last updated on 2013-11-19 16:38
The program
var next: Ref
method foo(this: Ref)
requires acc(this.next.next, wildcard)
{}
makes the parser fail with
Parse error: Failure: '(' expected but ',' found
Removing the second .next
makes the program getting parsed.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.