diff --git a/silver.sh b/silver.sh
new file mode 100755
index 000000000..383464af0
--- /dev/null
+++ b/silver.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+set -e
+
+BASEDIR="$(realpath "$(dirname "$0")")"
+
+CP_FILE="$BASEDIR/silver_classpath.txt"
+
+if [ ! -f "$CP_FILE" ]; then
+    (cd "$BASEDIR"; sbt "export runtime:dependencyClasspath" | tail -n1 > "$CP_FILE")
+fi
+
+exec java -cp "$(cat "$CP_FILE")" viper.silver.SilverRunner "$@"
diff --git a/src/main/scala/viper/silver/SilverRunner.scala b/src/main/scala/viper/silver/SilverRunner.scala
new file mode 100644
index 000000000..0aaa8188b
--- /dev/null
+++ b/src/main/scala/viper/silver/SilverRunner.scala
@@ -0,0 +1,28 @@
+package viper.silver
+
+
+import scala.collection.immutable.ArraySeq
+import viper.silver.frontend.DefaultStates 
+import viper.silver.frontend.ViperAstProvider
+import viper.silver.logger.SilentLogger
+import viper.silver.reporter.NoopReporter
+
+
+object SilverRunner extends SilverRunnerInstance {
+  def main(args: Array[String]): Unit = {
+    runMain(args)
+  }
+}
+
+class SilverRunnerInstance extends ViperAstProvider(NoopReporter, SilentLogger().get) {
+  def runMain(args: Array[String]): Unit = {
+    var exitCode = 1 /* Only 0 indicates no error */
+
+    execute(ArraySeq.unsafeWrapArray(args))
+    
+    if (state >= DefaultStates.Translation) {
+      exitCode = 0
+    }
+    sys.exit(exitCode)
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala
index 1502bf1ac..09d03f619 100644
--- a/src/main/scala/viper/silver/parser/FastParser.scala
+++ b/src/main/scala/viper/silver/parser/FastParser.scala
@@ -33,7 +33,7 @@ object FastParserCompanion {
   implicit val whitespace = {
     import NoWhitespace._
     implicit ctx: ParsingRun[_] =>
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
+      NoTrace((("/*" ~ (!"*/" ~ AnyChar).rep ~ "*/") | ((("//" ~ !("/")) | "////") ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
   }
 
   def identStarts[$: P] = CharIn("A-Z", "a-z", "$_")
@@ -312,14 +312,7 @@ class FastParser {
   //////////////////////////
 
   import fastparse._
-  import FastParserCompanion.{ExtendedParsing, identContinues, identStarts, LeadingWhitespace, Pos, PositionParsing, reservedKw, reservedSym}
-
-
-  implicit val whitespace = {
-    import NoWhitespace._
-    implicit ctx: ParsingRun[_] =>
-      NoTrace((("/*" ~ (!StringIn("*/") ~ AnyChar).rep ~ "*/") | ("//" ~ CharsWhile(_ != '\n').? ~ ("\n" | End)) | " " | "\t" | "\n" | "\r").rep)
-  }
+  import FastParserCompanion.{ExtendedParsing, identContinues, identStarts, LeadingWhitespace, Pos, PositionParsing, reservedKw, reservedSym, whitespace}
 
   implicit val lineCol: LineCol = new LineCol(this)
 
@@ -403,7 +396,11 @@ class FastParser {
 
   def stringLiteral[$: P]: P[PStringLiteral] = P((CharsWhile(_ != '\"').! map PRawString.apply).pos.quotes map (PStringLiteral.apply _)).pos
 
-  def annotation[$: P]: P[PAnnotation] = P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAnnotation.apply _).tupled).pos
+  def docString[$: P]: P[PRawString] = P(CharsWhile(_ != '\n', 0).! map PRawString.apply).pos
+
+  def docAnnotation[$: P]: P[PAnnotation] = P(P(PSym.TripleSlash) ~~ docString).map{ case (s, d) => p => PDocAnnotation(s, d)(p) }.pos
+
+  def annotation[$: P]: P[PAnnotation] = P(P((P(PSym.At) ~~ annotationIdentifier ~ argList(stringLiteral)) map (PAtAnnotation.apply _).tupled).pos | docAnnotation)
 
   def annotated[$: P, T](inner: => P[PAnnotationsPosition => T]): P[T] = P((annotation.rep(0) ~ inner).map {
     case (annotations, i) => pos: Pos => i(PAnnotationsPosition(annotations, pos))
@@ -486,7 +483,7 @@ class FastParser {
 
   def suffixExpr[$: P](bracketed: Boolean = false): P[PExp] = P((atomParen(bracketed) ~~~ suffix.lw.rep).map { case (fac, ss) => foldPExp(fac, ss) })
 
-  def termOp[$: P] = P(reservedSymMany(None, StringIn("*", "/", "\\", "%"), _ match {
+  def termOp[$: P] = P(reservedSymMany(None, !("///") ~ StringIn("*", "/", "\\", "%"), _ match {
     case "*" => PSymOp.Mul
     case "/" => PSymOp.Div
     case "\\" => PSymOp.ArithDiv
@@ -807,9 +804,15 @@ class FastParser {
     P((P(PKw.Else) ~ stmtBlock()) map (PElse.apply _).tupled).pos
 
   def whileStmt[$: P]: P[PKw.While => Pos => PWhile] =
-    P((parenthesizedExp ~~ semiSeparated(invariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile(_, cond, invs, body) })
+    P((parenthesizedExp ~~ semiSeparated(annotatedInvariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile(_, cond, invs, body) })
 
-  def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] = P((P(PKw.Invariant) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.invSpecification(ctx))
+  def annotatedInvariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
+    NoCut(P(annotation.rep(0) ~ invariant)).map{ case (anns, spec) => p: Pos =>
+            PSpecification[PKw.InvSpec](spec.k, spec.e, anns)(p) }.pos
+
+  def invariant(implicit ctx : P[_]) : P[PSpecification[PKw.InvSpec]] =
+    P((P(PKw.Invariant) ~ exp).map{ case (kw, e) => p: Pos =>
+      PSpecification[PKw.InvSpec](kw, e)(p) }.pos | ParserExtension.invSpecification(ctx))
 
   def localVars[$: P]: P[PKw.Var => Pos => PVars] =
     P((nonEmptyIdnTypeList(PLocalVarDecl(_)) ~~~ (P(PSymOp.Assign) ~ exp).lw.?) map { case (a, i) => PVars(_, a, i) })
@@ -824,7 +827,7 @@ class FastParser {
   def goto[$: P]: P[PKw.Goto => Pos => PGoto] = P(idnref[$, PLabel] map { i => PGoto(_, i) _ })
 
   def label[$: P]: P[PKw.Label => Pos => PLabel] =
-    P((idndef ~~ semiSeparated(invariant)) map { case (i, inv) => k=> PLabel(k, i, inv) _ })
+    P((idndef ~~ semiSeparated(annotatedInvariant)) map { case (i, inv) => k=> PLabel(k, i, inv) _ })
 
   def packageWand[$: P]: P[PKw.Package => Pos => PPackageWand] =
     P((magicWandExp() ~~~ stmtBlock().lw.?) map { case (wand, proof) => PPackageWand(_, wand, proof) _ })
@@ -915,15 +918,26 @@ class FastParser {
   })
 
   def functionDecl[$: P]: P[PKw.Function => PAnnotationsPosition => PFunction] = P((idndef ~ argList(formalArg) ~ PSym.Colon ~ typ
-    ~~ semiSeparated(precondition) ~~ semiSeparated(postcondition) ~~~ bracedExp.lw.?
+    ~~ semiSeparated(annotatedPrecondition) ~~ semiSeparated(annotatedPostcondition) ~~~ bracedExp.lw.?
   ) map { case (idn, args, c, typ, d, e, f) => k =>
       ap: PAnnotationsPosition => PFunction(ap.annotations, k, idn, args, c, typ, d, e, f)(ap.pos)
   })
 
+  def annotatedPrecondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
+    NoCut(P(annotation.rep(0) ~ precondition)).map{ case (anns, spec) => p: Pos =>
+            PSpecification[PKw.PreSpec](spec.k, spec.e, anns)(p) }.pos
+
+  def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] =
+    P((P(PKw.Requires) ~ exp).map{ case (kw, e) => p: (FilePosition, FilePosition) =>
+        PSpecification[PKw.PreSpec](kw, e)(p)}.pos | ParserExtension.preSpecification(ctx))
 
-  def precondition(implicit ctx : P[_]) : P[PSpecification[PKw.PreSpec]] = P((P(PKw.Requires) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.preSpecification(ctx))
+  def annotatedPostcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
+    NoCut(P(annotation.rep(0) ~ postcondition)).map{ case (anns, spec) => p: Pos =>
+      PSpecification[PKw.PostSpec](spec.k, spec.e, anns)(p) }.pos
 
-  def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] = P((P(PKw.Ensures) ~ exp).map((PSpecification.apply _).tupled).pos | ParserExtension.postSpecification(ctx))
+  def postcondition(implicit ctx : P[_]) : P[PSpecification[PKw.PostSpec]] =
+    P((P(PKw.Ensures) ~ exp).map{ case (kw, e) => p: Pos =>
+        PSpecification[PKw.PostSpec](kw, e)(p)}.pos | ParserExtension.postSpecification(ctx))
 
   def predicateDecl[$: P]: P[PKw.Predicate => PAnnotationsPosition => PPredicate] = P(idndef ~ argList(formalArg) ~~~ bracedExp.lw.?).map {
     case (idn, args, c) => k =>
@@ -931,7 +945,7 @@ class FastParser {
   }
 
   def methodDecl[$: P]: P[PKw.Method => PAnnotationsPosition => PMethod] =
-    P((idndef ~ argList(formalArg) ~~~ methodReturns.lw.? ~~ semiSeparated(precondition) ~~ semiSeparated(postcondition) ~~~ stmtBlock().lw.?) map {
+    P((idndef ~ argList(formalArg) ~~~ methodReturns.lw.? ~~ semiSeparated(annotatedPrecondition) ~~ semiSeparated(annotatedPostcondition) ~~~ stmtBlock().lw.?) map {
         case (idn, args, rets, pres, posts, body) => k =>
           ap: PAnnotationsPosition => PMethod(ap.annotations, k, idn, args, rets, pres, posts, body)(ap.pos)
     })
diff --git a/src/main/scala/viper/silver/parser/ParseAst.scala b/src/main/scala/viper/silver/parser/ParseAst.scala
index 539a80fa8..d4fc8a349 100644
--- a/src/main/scala/viper/silver/parser/ParseAst.scala
+++ b/src/main/scala/viper/silver/parser/ParseAst.scala
@@ -1668,7 +1668,7 @@ case class PFields(annotations: Seq[PAnnotation], field: PKw.Field, fields: PDel
   override def declares: Seq[PGlobalDeclaration] = fields.toSeq
 }
 
-case class PSpecification[+T <: PKw.Spec](k: PReserved[PKw.Spec], e: PExp)(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
+case class PSpecification[+T <: PKw.Spec](k: PReserved[PKw.Spec], e: PExp, annotations: Seq[PAnnotation] = Seq())(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
   override def pretty: String = "\n  " + super.pretty
 }
 
@@ -1694,10 +1694,15 @@ case class PMethodReturns(k: PKw.Returns, formalReturns: PGrouped.Paren[PDelimit
   */
 case class PAnnotationsPosition(annotations: Seq[PAnnotation], pos: (FilePosition, FilePosition))
 
-case class PAnnotation(at: PSym.At, key: PRawString, values: PGrouped.Paren[PDelimited[PStringLiteral, PSym.Comma]])(val pos: (Position, Position)) extends PNode with PPrettySubnodes {
+sealed trait PAnnotation extends PNode with PPrettySubnodes {
+  def key: PRawString
   override def pretty: String = super.pretty + "\n"
 }
 
+case class PAtAnnotation(at: PSym.At, key: PRawString, values: PGrouped.Paren[PDelimited[PStringLiteral, PSym.Comma]])(val pos: (Position, Position)) extends PNode with PAnnotation with PPrettySubnodes {}
+
+case class PDocAnnotation(tripleSlash: PSym.TripleSlash, docString: PRawString, key: PRawString = PRawString("doc")(NoPosition, NoPosition))(val pos: (Position, Position)) extends PAnnotation {}
+
 // Any unenclosed string (e.g. `hello`)
 case class PRawString(str: String)(val pos: (Position, Position)) extends PNode with PLeaf {
   override def display: String = str
diff --git a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
index 646c14819..78a3bc2a1 100644
--- a/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
+++ b/src/main/scala/viper/silver/parser/ParseAstKeyword.scala
@@ -321,6 +321,9 @@ object PSym {
   // Used for annotations
   case object At extends PSym("@") with PSymbolLang
   type At = PReserved[At.type]
+  // Used for documentation
+  case object TripleSlash extends PSym("///") with PSymbolLang
+  type TripleSlash = PReserved[TripleSlash.type]
   // Used for `new(*)`
   case object Star extends PSym("*") with PSymbolLang
   type Star = PReserved[Star.type]
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index ecc2fc4ec..8f99805f7 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -81,7 +81,9 @@ case class Translator(program: PProgram) {
 
       val newBody = body.map(actualBody => stmt(actualBody).asInstanceOf[Seqn])
 
-      val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(m.pos, m.info, m.errT)
+      val finalMethod = m.copy(pres = pres.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                               posts = posts.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                               body = newBody)(m.pos, m.info, m.errT)
 
       members(m.name) = finalMethod
 
@@ -107,7 +109,9 @@ case class Translator(program: PProgram) {
   private def translate(f: PFunction): Function = f match {
     case PFunction(_, _, idndef, _, _, _, pres, posts, body) =>
       val f = findFunction(idndef)
-      val ff = f.copy( pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = body map (_.e.inner) map exp)(f.pos, f.info, f.errT)
+      val ff = f.copy( pres = pres.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                       posts = posts.toSeq map (p => exp(wrapAnnotations(p.annotations, p.e)(p.pos))),
+                       body = body map (_.e.inner) map exp)(f.pos, f.info, f.errT)
       members(f.name) = ff
       ff
   }
@@ -232,7 +236,8 @@ case class Translator(program: PProgram) {
         }) getOrElse Statements.EmptyStmt)(pos, info)
       case PElse(_, els) => stmt(els)
       case PWhile(_, cond, invs, body) =>
-        While(exp(cond.inner), invs.toSeq map (inv => exp(inv.e)), stmt(body).asInstanceOf[Seqn])(pos, info)
+        While(exp(cond.inner), invs.toSeq map (inv => exp(wrapAnnotations(inv.annotations, inv.e)(inv.pos))),
+              stmt(body).asInstanceOf[Seqn])(pos, info)
       case PQuasihavoc(_, lhs, e) =>
         val (newLhs, newE) = havocStmtHelper(lhs, e)
         Quasihavoc(newLhs, newE)(pos, info)
@@ -313,16 +318,33 @@ case class Translator(program: PProgram) {
     }
   }
 
+  def wrapAnnotations(annotations: Seq[PAnnotation], pexp: PExp)(pos: (Position, Position)): PExp =
+    annotations.foldRight(pexp) { (ann, e) => new PAnnotatedExp(ann, e)(pos) }
+
   def extractAnnotation(pexp: PExp): (PExp, Map[String, Seq[String]]) = {
     pexp match {
       case PAnnotatedExp(ann, e) =>
         val (resPexp, innerMap) = extractAnnotation(e)
-        val combinedValue = if (innerMap.contains(ann.key.str)) {
-          ann.values.inner.toSeq.map(_.str) ++ innerMap(ann.key.str)
-        } else {
-          ann.values.inner.toSeq.map(_.str)
+        val key = ann match {
+          case ann: PAtAnnotation => ann.key.str
+          case ann: PDocAnnotation => "doc"
         }
-        (resPexp, innerMap.updated(ann.key.str, combinedValue))
+        val combinedValue =
+          ann match {
+            case ann: PAtAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.values.inner.toSeq.map(_.str) ++ innerMap(key)
+              } else {
+                ann.values.inner.toSeq.map(_.str)
+              }
+            case ann: PDocAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.docString.str +: innerMap(key)
+              } else {
+                Seq(ann.docString.str)
+              }
+          }
+        (resPexp, innerMap.updated(key, combinedValue))
       case _ => (pexp, Map())
     }
   }
@@ -331,12 +353,26 @@ case class Translator(program: PProgram) {
     pStmt match {
       case PAnnotatedStmt(ann, s) =>
         val (resPStmt, innerMap) = extractAnnotationFromStmt(s)
-        val combinedValue = if (innerMap.contains(ann.key.str)) {
-          ann.values.inner.toSeq.map(_.str) ++ innerMap(ann.key.str)
-        } else {
-          ann.values.inner.toSeq.map(_.str)
+        val key = ann match {
+          case ann: PAtAnnotation => ann.key.str
+          case ann: PDocAnnotation => "doc"
         }
-        (resPStmt, innerMap.updated(ann.key.str, combinedValue))
+        val combinedValue =
+          ann match {
+            case ann: PAtAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.values.inner.toSeq.map(_.str) ++ innerMap(key)
+              } else {
+                ann.values.inner.toSeq.map(_.str)
+              }
+            case ann: PDocAnnotation =>
+              if (innerMap.contains(key)) {
+                ann.docString.str +: innerMap(key)
+              } else {
+                Seq(ann.docString.str)
+              }
+          }
+        (resPStmt, innerMap.updated(key, combinedValue))
       case _ => (pStmt, Map())
     }
   }
@@ -723,7 +759,9 @@ object Translator {
     if (annotations.isEmpty) {
       NoInfo
     } else {
-      AnnotationInfo(annotations.groupBy(_.key).map{ case (k, v) => k.str -> v.flatMap(_.values.inner.toSeq.map(_.str)) })
+      AnnotationInfo(annotations.groupBy(_.key).map{ case (k, v) => k.str -> v.flatMap{
+                         case a: PAtAnnotation => a.values.inner.toSeq.map(_.str)
+                         case a: PDocAnnotation => Seq(a.docString.str) }})
     }
   }
 }
diff --git a/src/main/scala/viper/silver/plugin/standard/doc/DocPlugin.scala b/src/main/scala/viper/silver/plugin/standard/doc/DocPlugin.scala
new file mode 100644
index 000000000..e2b095e6c
--- /dev/null
+++ b/src/main/scala/viper/silver/plugin/standard/doc/DocPlugin.scala
@@ -0,0 +1,138 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2019 ETH Zurich.
+
+package viper.silver.plugin.standard.doc
+
+import viper.silver.plugin.SilverPlugin
+import viper.silver.ast.{Program, FilePosition, NoPosition, Position}
+import viper.silver.parser.{PProgram, PFieldDecl, PFields, PNode, PAnnotated, PAnnotatedExp,
+  PAnnotatedStmt, PAnnotation, PAtAnnotation, PDocAnnotation, PMethod, PFunction, PStringLiteral,
+  PAxiom, PSpecification, PRawString, PIdnRef, PPredicate, PDomain, PDomainFunction, Translator}
+import viper.silver.ast.utility.Visitor
+import upickle.default._
+import java.io._
+import viper.silver.frontend.SilFrontend
+import viper.silver.verifier.ParseReport
+
+case class DocReport(message: String, override val pos: Position)
+  extends ParseReport(message, pos) {
+  def fullId = "parser.documentation"
+  def readableMessage = message
+}
+
+class DocPlugin extends SilverPlugin {
+
+  case class DocNode(nodeType: String, info: NodeInfo, pos: (String, String), doc: String = "", children: Seq[DocNode]) {
+    /** @see [[Visitor.reduceTree()]] */
+    def reduceTree[T](f: (DocNode, Seq[T]) => T) = Visitor.reduceTree(this, DocNode.callSubnodes)(f)
+
+    /** @see [[Visitor.reduceWithContext()]] */
+    def reduceWithContext[C, R](context: C, enter: (DocNode, C) => C, combine: (DocNode, C, Seq[R]) => R) = {
+      Visitor.reduceWithContext(this, DocNode.callSubnodes)(context, enter, combine)
+    }
+  }
+
+  object DocNode {
+    def callSubnodes(n: DocNode): Seq[DocNode] = n.children
+    implicit lazy val rw: ReadWriter[DocNode] = macroRW
+  }
+
+  case class VarInfo(name: String, typ: String)
+  case class NodeInfo(name: String = "", typ: String = "",
+                      args: Seq[VarInfo] = Seq(),
+                      returns: Seq[VarInfo] = Seq(),
+                      misc: String = "")
+
+  object VarInfo {
+    implicit lazy val rw: ReadWriter[VarInfo] = macroRW
+  }
+  object NodeInfo {
+    implicit lazy val rw: ReadWriter[NodeInfo] = macroRW
+  }
+
+  /** Called after identifiers have been resolved but before the parse AST is
+    * translated into the normal AST.
+    *
+    * @param input
+    *   Parse AST
+    * @return
+    *   Modified Parse AST
+      */
+  override def beforeTranslate(input: PProgram): PProgram = {
+    val extractInfo: PNode => NodeInfo = {
+      // case n: PFields => Map("name" -> n.toString())
+      case PIdnRef(name) => NodeInfo(name)
+      case PFieldDecl(idndef, colon, typ) => NodeInfo(idndef.name, typ.toString())
+      case n: PMethod =>
+        NodeInfo(n.idndef.name, "", n.args.inner.toSeq.map(a => VarInfo(a.idndef.name, a.typ.toString())),
+                 n.returns match {
+                   case Some(returns) => returns.formalReturns.inner.toSeq.map(a => VarInfo(a.idndef.name, a.typ.toString()))
+                   case None => Seq() })
+      case n: PFunction =>
+        NodeInfo(n.idndef.name, n.resultType.toString(),
+                 n.args.inner.toSeq.map(a => VarInfo(a.idndef.name, a.typ.toString())))
+      case n: PPredicate => NodeInfo(n.idndef.name, "", n.args.inner.toSeq.map(a => VarInfo(a.idndef.name, a.typ.toString())))
+      case n: PDomain =>
+        NodeInfo(n.idndef.name, "",
+                 n.typVars match {
+                   case Some(typVars) => typVars.inner.toSeq.map(a => VarInfo("", a.idndef.name))
+                   case None => Seq() })
+      case n: PDomainFunction =>
+        NodeInfo(n.idndef.name, n.resultType.toString(),
+                 n.args.inner.toSeq.map(a =>
+                   VarInfo(a.name match {case Some(idndef) => idndef.name case None => ""}, a.typ.toString())),
+                 Seq(), n.unique match {case Some(kw) => kw.display.trim() case None => ""})
+      case n: PAxiom =>
+        NodeInfo(n.idndef match {case Some(id) => id.name case None => ""})
+      case n: PSpecification[_] => NodeInfo(n.k.rs.display.trim())
+      case _ => NodeInfo()
+    }
+
+    val extractPos: PNode => (String, String) = n => (n.pos._1.toString(), n.pos._2.toString())
+
+    val collectDocs: Seq[PAnnotation] => String = _.collect{ case k: PAtAnnotation if (k.key.str == "doc") => k.values.inner.toSeq.map(_.str)
+      case k: PDocAnnotation => Seq(k.docString.str) }.flatten.mkString("\n")
+    val translator: Translator = new Translator(input);
+    val extractDoc: PNode => String =
+      ({
+         case e: PAnnotatedExp => translator.extractAnnotation(e)._2.getOrElse("doc", Seq()).mkString("\n")
+         case s: PAnnotatedStmt => translator.extractAnnotationFromStmt(s)._2.getOrElse("doc", Seq()).mkString("\n")
+         case n: PAnnotated => collectDocs(n.annotations)
+         case n: PSpecification[_] => collectDocs(n.annotations)
+         case n: PAxiom => collectDocs(n.annotations)
+         case _ => ""
+       }: PNode => String)
+
+    val removeRoots: Seq[DocNode] => Seq[DocNode] = s => s.flatMap{
+      case t: DocNode if (t.nodeType == "*root*") => t.children
+      case n: DocNode => Seq(n)
+    }
+
+    val docTree = input.reduceTree(
+      (n: PNode, children: Seq[DocNode]) => {
+        val createDocNode = ((kind: String, n: PNode) =>
+          DocNode(kind, extractInfo(n), extractPos(n), extractDoc(n), removeRoots(children)))
+
+        n match {
+          case n: PIdnRef[_]                 => createDocNode("IdnRef", n)
+          case n: PFieldDecl                 => createDocNode("FieldDecl", n)
+          case n: PMethod                    => createDocNode("Method", n)
+          case n: PFunction                  => createDocNode("Function", n)
+          case n: PSpecification[_]          => createDocNode("Specification", n)
+          case n: PPredicate                 => createDocNode("Predicate", n)
+          case n: PDomain                    => createDocNode("Domain", n)
+          case n: PAxiom                     => createDocNode("Axiom", n)
+          case n: PDomainFunction            => createDocNode("DomainFunction", n)
+          case _                             => DocNode("*root*", NodeInfo(), ("", ""), "", removeRoots(children))
+        }
+      })
+
+    val json: String = write(docTree)
+    println(json)
+
+    PProgram(input.imported, input.members)(input.pos, DocReport(json, NoPosition) +: input.localErrors)
+  }
+}
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index a77b9ff91..519972442 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -8,7 +8,7 @@ package viper.silver.plugin.standard.termination
 
 import viper.silver.ast.utility.{Functions, ViperStrategy}
 import viper.silver.ast.utility.rewriter.{SimpleContext, Strategy, StrategyBuilder}
-import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, FuncApp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
+import viper.silver.ast.{Applying, Assert, CondExp, CurrentPerm, Exp, FilePosition, FuncApp, Function, InhaleExhaleExp, MagicWand, Method, Node, Program, Unfolding, While}
 import viper.silver.parser._
 import viper.silver.plugin.standard.predicateinstance.{PMarkerSymbol, PPredicateInstance}
 import viper.silver.plugin.standard.termination.transformation.Trafo
@@ -45,7 +45,8 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
    * decreases *
    */
   def decreases[$: P]: P[PSpecification[PDecreasesKeyword.type]] =
-    P((P(PDecreasesKeyword) ~ (decreasesWildcard | decreasesStar | decreasesTuple)) map (PSpecification.apply _).tupled).pos
+    P((P(PDecreasesKeyword) ~ (decreasesWildcard | decreasesStar | decreasesTuple)) map {
+        case (k, e) => p: (FilePosition, FilePosition) => PSpecification(k, e)(p) }).pos
   def decreasesTuple[$: P]: P[PDecreasesTuple] =
     P((exp.delimited(PSym.Comma) ~~~ condition.lw.?) map (PDecreasesTuple.apply _).tupled).pos
   def decreasesWildcard[$: P]: P[PDecreasesWildcard] = P((P(PWildcardSym) ~~~ condition.lw.?) map (PDecreasesWildcard.apply _).tupled).pos
@@ -239,7 +240,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
    * Remove decreases clauses from the AST and add them as information to the AST nodes
    */
   override def beforeVerify(input: Program): Program = {
-    // Prevent potentially unsafe (mutually) recursive function calls in function postcondtions
+    // Prevent potentially unsafe (mutually) recursive function calls in function postconditions
     // for all functions that don't have a decreases clause
     if (!deactivated) {
       lazy val cycles = Functions.findFunctionCyclesViaOptimized(input, func => func.body.toSeq)
diff --git a/src/test/scala/DocAnnotationTests.scala b/src/test/scala/DocAnnotationTests.scala
new file mode 100644
index 000000000..16545a079
--- /dev/null
+++ b/src/test/scala/DocAnnotationTests.scala
@@ -0,0 +1,149 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2024 ETH Zurich.
+
+import org.scalatest.funsuite.AnyFunSuite
+import viper.silver.ast.Program
+import viper.silver.frontend._
+import viper.silver.logger.ViperStdOutLogger
+import viper.silver.reporter.StdIOReporter
+import viper.silver.parser.{PProgram, PAnnotatedExp, PWhile}
+
+class DocAnnotationTests extends AnyFunSuite {
+  object AstProvider extends ViperAstProvider(StdIOReporter(), ViperStdOutLogger("DocAnnotationTestsLogger").get) {
+    def setCode(code: String): Unit = {
+      _input = Some(code)
+    }
+
+    override def reset(input: java.nio.file.Path): Unit = {
+      if (state < DefaultStates.Initialized) sys.error("The translator has not been initialized.")
+      _state = DefaultStates.InputSet
+      _inputFile = Some(input)
+      /** must be set by [[setCode]] */
+      // _input = None
+      _errors = Seq()
+      _parsingResult = None
+      _semanticAnalysisResult = None
+      _verificationResult = None
+      _program = None
+      resetMessages()
+    }
+  }
+
+  def generatePAstAndAst(code: String): Option[(PProgram, Program)] = {
+    val code_id = code.hashCode.asInstanceOf[Short].toString
+    AstProvider.setCode(code)
+    AstProvider.execute(Seq("--ignoreFile", code_id))
+
+    if (AstProvider.errors.isEmpty) {
+      Some(AstProvider.parsingResult, AstProvider.translationResult)
+    } else {
+      AstProvider.logger.error(s"An error occurred while translating ${AstProvider.errors}")
+      None
+    }
+  }
+
+  test("Basic parsing of documentation") {
+    import viper.silver.ast._
+
+    val code =
+      """/// a field
+        |field f: Int
+        |/// P is a predicate
+        |predicate P(x: Int)
+        |
+        |/// a function
+        |function fun(x: Int): Int {
+        |  (x / 1 == x) ? 42 : 0
+        |}
+        |/// a second function
+        |function fun2(x: Int): Int
+        |    /// precondition
+        |    requires x > 0
+        |    /// post-
+        |    /// condition
+        |    ensures result > 0
+        |
+        |/// very important domain
+        |domain ImportantType {
+        |
+        |  /// this function
+        |  /// is crucial
+        |  function phi(ImportantType): Int
+        |
+        |  /// the only axiom
+        |  axiom {
+        |    /// documenting an expression
+        |    true
+        |  }
+        |}
+        |
+        |/// a macro
+        |define plus(a, b) (a+b)
+        |
+        |/// this is a method
+        |/// it does something
+        |method m(x: Ref, y: Ref)
+        |    /// this documents the first precondition
+        |    requires acc(x.f)
+        |    /// documentation of the second precondition
+        |    requires acc(y.f)
+        |{
+        |    var local: Bool
+        |
+        |    while (true)///the invariant
+        |      /// is always true
+        |      invariant true
+        |      /// termination
+        |      decreases x.f
+        |    {}
+        |
+        |}
+        |""".stripMargin
+
+    val pAst: PProgram = generatePAstAndAst(code).get._1
+
+    val fieldAnn = pAst.fields.head.annotations.head.values.inner.first.get.str
+    assert(fieldAnn == " a field")
+
+    val predicateAnnotation = pAst.predicates.head.annotations.head.values.inner.first.get.str
+    assert(predicateAnnotation == " P is a predicate")
+
+    val functionAnnotation = pAst.functions.head.annotations.head.values.inner.first.get.str
+    assert(functionAnnotation == " a function")
+
+    val fun2Annotation = pAst.functions(1).annotations.head.values.inner.first.get.str
+    val fun2PreAnnotations = pAst.functions(1).pres.head.annotations.map(_.values.inner.first.get.str)
+    val fun2PostAnnotations = pAst.functions(1).posts.head.annotations.map(_.values.inner.first.get.str)
+    assert(fun2Annotation == " a second function")
+    assert(fun2PreAnnotations == Seq(" precondition"))
+    assert(fun2PostAnnotations == Seq(" post-", " condition"))
+
+    val domainAnnotation = pAst.domains.head.annotations.head.values.inner.first.get.str
+    assert(domainAnnotation == " very important domain")
+
+    val domainFunctionAnnotations = pAst.domains.head.members.inner.funcs.head.annotations.map(_.values.inner.first.get.str)
+    assert(domainFunctionAnnotations == Seq(" this function", " is crucial"))
+
+    val axiomAnnotations = pAst.domains.head.members.inner.axioms.head.annotations.map(_.values.inner.first.get.str)
+    assert(axiomAnnotations == Seq(" the only axiom"))
+    val axiomExpAnnotations = pAst.domains.head.members.inner.axioms.head.exp.e.inner.asInstanceOf[PAnnotatedExp].annotation.values.inner.first.get.str
+    assert(axiomExpAnnotations == " documenting an expression")
+
+    val macroAnnotation = pAst.macros.head.annotations.head.values.inner.first.get.str
+    assert(macroAnnotation == " a macro")
+
+    val methodAnnotations = pAst.methods.head.annotations.map(_.values.inner.first.get.str)
+    assert(methodAnnotations == Seq(" this is a method", " it does something"))
+
+    val methodPreAnnotations = pAst.methods.head.pres.toSeq.map(_.annotations.head.values.inner.first.get.str)
+    assert(methodPreAnnotations == Seq(" this documents the first precondition", " documentation of the second precondition"))
+
+    val loopInvariantAnnotations = pAst.methods.head.body.get.ss.inner.inner.collect {
+          case (_, w: PWhile) => w.invs.toSeq.flatMap(_.annotations.map(_.values.inner.first.get.str))
+    }.flatten
+    assert(loopInvariantAnnotations == Seq("the invariant", " is always true", " termination"))
+  }
+}
\ No newline at end of file