Program Semantics, Verification, and Construction

(Previous instance: 2007/2008)

2008/2009

Course coordinator: Nelma Moreira (nam(AT)ncc(DOT)up(DOT)pt)

Lecture 1

Lambda Calculus

Date:

Notes:

Lecture 2

Deduction Systems and Intuitionism

Date:

Notes:

* psvc02.pdf

Lecture 3

Type systems and the Curry-Howard isomorphism

Date:

Notes:

• Simple Types

• Curry-Howard Iso.

• gallier91constructive.pdf: Constructive Logics: part 1 , J. Gallier

• lectures-on-the-curry.pdf: Lectures on Curry-Howard Isomorphism

Lecture 4

Operational Semantics

Bibliography:

Semantics with Applications, H. Nielson and F. Nielson. (online version)

Date:

Lecture 5

Denotational Semantics

Date:

Bibliography:

Semantics with Applications, H. Nielson and F. Nielson. (online version)

Lecture 6

Proof assistants based on type theory

Date:

Notes:

• Type Systems and Logics (01-20) (21-30) (31-61)

Lecture 7

Extensions of Pure Type Systems

The Coq proof assistant

Date:

Notes:

• Beyond Pure Type Systems (01-20) (21-40)

• A Pratical Approach to the Coq System (Slides)(Proof script)(Exercises)

Material:

• Coq web page
• Coq Tutorial
• Coq in a Hurry - a tutorial by Yves Bertot (INRIA, Sophia-Antipolis)
• Coq-Lab - a pratical approach to Coq with exercises, by J-C Filliâtre and C. Paulin-Mohring.

Lecture 8

Functional Program Verification in Coq

Date:

Notes:

• Program Verification in Coq (Slides)(Proof script)

Lecture 9

Hoare logic and interface specification languages

Date:

Slides:

Lecture 10

Verification conditions and program verification in practice

Date:

Slides

Lecture 11

Introduction to the mathematics of program construction

Date:

Topics:Overview of the scientific method applied to software design.Correct by verification versus correct by construction. Calculate versus invent & verify.The e=m+c equation: description versus calculation. Point-free (PF) and point-wise (PW) notations. PF-transform for (algebraic) reasoning.

Notes:

• Theory and applications of the PF-transform Lectures 1-2 (01-56) (slides of the LerNET? doctoral school at Piriapolis, Uruguay, 2008)
• Full tutorial paper: (LNCS)

Lecture 12

PF-transform: when everything becomes a relation

Date:

Topics:

Taxonomy of binary relations. Functions. Conditions and coreflexives. PF-transform of n-ary relations. Products and Sums. Universal constructions and properties. Extended static checking (ESC) in the PF-style. Induction-free calculation of preconditions and invariants. Three case studies.

Notes:

• Theory and applications of the PF-transform Lectures 2-4 (57-124)

Lecture 13

Constructive proofs and program calculation

Date:

Topics:

A PF-approach to polymorphic type checking. Reynolds' relation on functions. The free-theorem of polymorphic functions in one equation. Inductive predicates and relations. The catamorphism concept. Universal property and its corollaries. Mutual recursion. Calculation of for/while loops from systems of mutually recursive equations over linear types.

Notes:

• Theorems for free: a (calculational) introduction (slides)

• Relational algebra: a Kleene algebra central to the mathematics of program construction (slides)

Program Semantics, Verification, and Construction

(Previous instance: 2008/2009)

2010/2011

Course leader: Jorge Sousa Pinto (jsp(AT)di(DOT)uminho(DOT)pt)

Lecture 1

Introduction to the mathematics of program construction

Date: 27/09/10 (Monday, 10h-13h). Room: DI A.1, Lecturer: J.N. Oliveira

Topics:

Notes:

• Theory and applications of the PF-transform Lectures 1-2 (01-56) (slides of the Ler-NET doctoral school at Piriapolis, Uruguay, 2008)
• Full tutorial paper: (LNCS)

Papers:

• zip

Lecture 2

PF-transform: when everything becomes a relation

Date:

Topics:

Taxonomy of binary relations. Functions. Conditions and coreflexives. PF-transform of n-ary relations. Union and meet. Universal constructions and properties. Galois connections underpinning relation algebra. Extended static checking(ESC) in the PF-style.

Notes:

• Theory and applications of the PF-transform Lectures 2-4 (57-124)

Lecture 3

PF-transform: extended static checking by calculation

Date:

Topics:

Notes:

• Hands on a Grand Challenge in Computing: Proving a Journaled File System Correct (PDF)

Lecture 4

Module assessment: paper recitation

Date:

Topics: Provisional schedule as follows:

• 10h00 - Carlos Eduardo Bastos e Marques da Silva: Variations on a Alloy-Centric Tool-chain in Verifying a Journaled File System Model
• 10h18 - Constantin Taivan: Reverse Program Calculation Supported by Code Slicing
• 10h36 - Frederico Miguel Goulão Valente: Generic Pointfree Lenses
• 10h54 - Henrique Manuel Fernandes de Castro: A Relational Model for Confined Separation Logic
• 11h12 Coffee break
• 11h30 - Nuno Filipe Moreira Macedo: First steps in Pointfree Functional Dependency Theory
• 11h48 - Nuno Miguel Almeida Luz: Strategic Term Rewriting and its Application to a VDM to SQL Convertion
• 12h06 - Paulo José Correia Bernardes: On the design of a Periodic Table of VDM specifications
• 12h24 - Eduardo Augusto Peixoto da Silva Brito: Tupling Calculation Eliminates Multiple Data Traversals
• 12h42 - Pedro Miguel Ribeiro Martins: Proving correctness using Free Theorems
• 13h00 Closing

Material:

Zip file containing all papers and presentations (11MB)

Lecture 5

A revision of propositional and first-order logics

Date:

Topics:

1. Propositional Logic (PL): Syntax; Semantics; Proof system; Adequacy of the proof system
2. First-Order Logic (FOL): Syntax; Semantics; Proof system; Theory for equality
3. Intuitionistic Logic: Natural deduction systems (propositional and first-order)

Notes:

• A revision of propositional and first-order logics (PDF)

Lecture 6

Validity Checking in Propositional and Forst-Order Logic

Date:

Topics:

1. Propositional Logic: general remarks; normal forms (NNF, CNF, DNF); validity/satisfiability in CNFs.
2. First-Order Logic: general remarks; normal forms (NNF, prenex, Herbrand/Skolem); Herbrand's theorem; semi-decidability; decidable fragments.
3. First-Order Theories: basic concepts; some theories of interest; SMT provers.

Notes:

• Validity Checking in Propositional and First-Order Logic (PDF)

Bibliography:

Any standard textbook on Mathematical Logic addresses most of the topics mentioned in the Lecture (e.g. [11] from the list of recommended books). A nice survey on the subject is

• Natarajan Shankar. Automated deduction for verification. ACM Computer Surveys, 41(4):1–56, 2009.

A more specialised list on the topic of decision procedures for specific theories:

• Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer Verlag, 2008.
• Aaron R. Bradley and Zohar Manna. Calculus of Computation: Decision Procedures with Applications to Verification. Springer Verlag, 2007.

Lecture 7

The λ-calculus and the Curry-Howard correspondence

Date:

Topics:

1. Proof Theory: Natural Deduction; Normalisation; Other proof systems
2. The λ-calculus: the untyped λ-calculus; the simply-typed λ-calculus
3. The Curry-Howard correspondence, variants, and uses

Notes:

• The λ-calculus and the Curry-Howard correspondence (PDF)

Bibliography:

• See references on the notes

Lecture 8

Type Systems and Logics

Date:

Topics:

1. Proof assistants based on type theory
2. Pure Type Systems
3. The Lambda Cube
4. The Logic Cube

Notes:

• Type Systems and Logics link (PDF)

Bibliography:

• Henk Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–309. Oxford Science Publications, 1992.
• Henk Barendregt and Herman Geuvers. Proof-assistants using dependent type systems. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 1149–1238. Elsevier and MIT Press, 2001.
• Gilles Barthe and Thierry Coquand. An introduction to dependent type theory. In Gilles Barthe, Peter Dybjer, Luís Pinto, and João Saraiva, editors, APPSEM, volume 2395 of Lecture Notes in Computer Science, pages 1–41. Springer, 2000.

Lecture 9

A Practical Approach to the Coq Proof-Assistant

Date:

Topics:

1. Gallina language (Coq specification language)
2. Interactive proof development environment
3. Case study: correctness of sorting algorithms

Notes:

• The Coq Proof-Assistant (PDF)

Bibliography:

• Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions, volume XXV of Texts in Theoretical Computer Science. An EATCS Series. Springer Verlag, 2004.
• Eduardo Giménez, Pierre Castéran. A Tutorial on Recursive Types in Coq.
(http://www.labri.fr/Perso/~casteran/RecTutorial.pdf.gz)
• Yves Bertot. Coq in a Hurry. (http://arxiv.org/abs/cs/0603118)
• Coq Reference Manual and Tutorial (downloadable from http://coq.inria.fr/)

Lecture 10

An Introduction to the Frama-C tool for the Analysis of C code

Date:

Topics:

1. Overview of formal code analysis and verification techniques: static analysis; abstract interpretation; software model checking; deductive verification
2. Introduction to Frama-C and its plugins
3. The Jessie tool: verification of safety properties of C code. The GWhy GUI and the multiprover facilities
4. The ACSL specification language. Verification of functional properties with Jessie.

Notes:

• Safety veriication with Frama-C (PDF)
• Functional Verification with Frama-C (PDF)

Bibliography:

• Loc Correnson, Pascal Cuoq, Armand Puccetti, and Julien Signoles. Frama-C user manual. from the Frama-C website, http://frama-c.com, 2010.
• Patrick Baudin, Jean-Christophe Fillitre, Claude March, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language. Preliminary Design (version 1.4). from the Frama-C website, http://frama-c.com, 2010.
• Yannick Moy and Claude March´e. Jessie Plugin Tutorial. LRI, February 2010. Beryllium Version.

-- Created by : JoseNunoOliveira - 24 Sep 2010

Part I

Write and present a short report in one of the topics.

Bibliography.

Formulae-as-types as a notion of control

Groups:

1. Bruno Oliveira and Vitor Rodrigues: Theme 5

2. Alexandre Madeira and Miguel Ferreira: Theme 1

3. Hugo Pacheco and Miguel Marques: Theme 2

4. Luis Santos and Ricardo Freitas: Theme 6

5. Hugo Conceição: Theme 3

6. José Pedro Oliveira: Theme 4

Part II

Coq mini-projects:

Binary Integers

The aim of this mini-project is to enconde binary integers as lists of booleans. That is:

Require Import ZArith.
Require Import List.
Require Import Bool.
Open Scope Z_scope.

Definition BInt := list bool.

Fixpoint toZ (x : BInt) : Z :=
 match x with
 | nil => 0
 | true :: xs => 1 + 2*(toZ xs)
 | false :: xs => 2*(toZ xs)
 end.

1. - Define the following functions:
   • bSucc - computes the successor of a binary integer
   • bAdd - computes the addition of two binary integers
   • bMult - computes multiplication of two binary integers
2. - Prove the correctness of those functions (e.g. forall x, toZ (bSucc x)=1+(toZ x))

NOTE: in the definition of bAdd, it is convenient to simultaneously define a function bAddCarry (performs addition with carry). Use the "Fixpoint ... with ..." to accomplish these simultaneous definitions.

Declarative Arrays

A possible encoding of arrays in Coq is through axiomatization of the corresponding theory. E.g. (taken from the Why tool)

(* The type of arrays *)
Parameter raw_array : Set -> Set.
Definition array (T:Set) := prod Z (raw_array T).

(* Array length *)
Definition array_length (T:Set) (t:array T) : Z := let (n, _) := t in n.

(* Functions to create, access and modify arrays *)
Parameter raw_new : forall T:Set, T -> raw_array T.
Definition new (T:Set) (n:Z) (a:T) : array T := (n, raw_new a).
Parameter raw_access : forall T:Set, raw_array T -> Z -> T.
Definition access (T:Set) (t:array T) (i:Z) : T :=
  let (_, r) := t in raw_access r i.
Parameter
  raw_update : forall T:Set, raw_array T -> Z -> T -> raw_array T.
Definition update (T:Set) (t:array T) (i:Z) (v:T) : array T :=
  (array_length t, let (_, r) := t in raw_update r i v).

(* Update does not change length *)
Lemma array_length_update :
 forall (T:Set) (t:array T) (i:Z) (v:T),
   array_length (update t i v) = array_length t.
Proof.
trivial.
Qed.

(* Axioms *)
Axiom
  new_def :
    forall (T:Set) (n:Z) (v0:T) (i:Z),
      (0 <= i < n)%Z -> access (new n v0) i = v0.

Axiom
  update_def_1 :
    forall (T:Set) (t:array T) (v:T) (i:Z),
      (0 <= i < array_length t)%Z -> access (update t i v) i = v.

Axiom
  update_def_2 :
    forall (T:Set) (t:array T) (v:T) (i j:Z),
      (0 <= i < array_length t)%Z ->
      (0 <= j < array_length t)%Z ->
      i <> j -> access (update t i v) j = access t j.

1. - Define a function sumArray to compute the sum of elements in an array.
2. - Formulate and prove the correctness of the previously defined function.

Paper Reading

• A Tutorial on Recursive Types in Coq. Eduardo Gimenez and Pierre Casteran. link

• Efficient Weakest Preconditions. K. Rustan M. Leino. link

• Boogie: A Modular Reusable Verifier for Object-Oriented Programs. Mike Barnett, Bor-Yuh Evan Chang, Robert deLine, Bart Jacobs, and K. Rustan M. Leino. link

• A Certifying Compiler for Java. Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, Kenneth Cline. link

• Foundational Proof-Carrying Code. Andrew W. Appel. link

• Proof Obligations Preserving Compilation (Extended abstract). Gilles Barthe, Tamara Rezk and Ando Saabas. link

• Universes: Lightweight Ownership for JML. Werner Dietl and Peter Mueller. link

• Beyond Assertions: Advanced Specification and Verification with JML and ESC / Java2. Patrice Chalin, Joseph Kiniry, Gary T. Leavens and Erki Poll. link

Part III

Workshop "Program Semantics, Verification, and Construction" 16/02/2008

10h-11h45 Part 1:

1. Alexandre Madeira, Miguel Ferreira. "Combinatory logic"

2. Hugo Pacheco. "Expressibility: the simply typed lambda-calculus (vs. the pure system), system T"

3. Bruno Oliveira, Vitor Rodrigues. "Type systems I"

4. Luis Santos, Ricardo Freitas. "Type system II"

Part 2: 12h-13h45

1. Bruno Oliveira. "Efficient Weakest Preconditions"

2. Vitor Rodrigues, Ricado Freitas. "Beyond assertions: Advanced specification and verification with JML and ESC/Java2"

3. Alexandre Madeira. "Pointfree Factorization of Operation Refinement"

4. Hugo Pacheco. "Tupling calculation eliminates multiple data traversal"

Results

Part I

• Paper reading and presentations

Part II

• Home assessment: Home exam to be delivered by January 10.

Part III

-- JorgeSousaPinto - 07 Dec 2010

Recommended Books

1. Samson Abramsky and Achim Jung. Domain theory. In Handbook of Logic in Computer Science (vol. 3): Semantic Structures, pages 1?168. Oxford University Press, Oxford, UK, 1994.
2. Roland C. Backhouse. Program construction and verification. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986.
3. Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, second, revised edition, 1984.
4. Henk P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 2, pages 117?309. Oxford University Press, 1992.
5. Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. Springer Verlag, 2004.
6. Richard Bird and Oege de Moor. Algebra of Programming. Prentice Hall, 1997.
7. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. (online version)
8. M. Hennessy. The Semantics of Programming Languages. Wiley, 1990.
9. H. R. Nielson and F. Nielson. Semantics with Applications : A Formal Introduction. Wiley, 1992. (online version)
10. Glynn Winskel. The Formal Semantics of Programming Languages: An introduction. Foundations of Computing. The MIT Press, Cambridge, Massachusetts, 1993.
11. Jean Goubault-Larrecq and Ian Mackie. Proof Theory and Automated Deduction. Kluwer Academic Press, 1997.

Chapter I: Overview of Foundations

1. Intuitionistic logic
2. Natural deduction
3. lambda-calculus (terms, reduction, the Church-Rosser Theorem)
4. Simple Types (Church versus Curry typing, normalization, extensions)
5. The Curry-Howard isomorphism
6. Introduction to operational semantics
7. Domain theory (complete partial orders, continuous functions)
8. Denotational semantics

Chapter II: Program Verification

1. Dependent Types:
   • First-order dependent types
   • Type equivalence
   • Sum types
   • The calculus of inductive constructions
   • Programming with dependent types
2. Type-based proof assistants
   • Interactive proof development
   • Tactics and tacticals
   • Inductive data types and predicates
3. Program correctness: specification; partial and total correctness
4. Verification of the correctness of functional programs:
   • Extraction of the computational contents of a correctness proof
   • Using programs for structuring correction proofs
5. Axiomatic semantics of imperative programs:
   • Assertions; semantics of assertions
   • Hoare proof rules for correctness
6. Tool support for the specification, verification, and certification of programs:
   • Proof assistants
   • Verification condition generators
7. Alternative approaches to program verification
   • Certifying compilation and proof-carrying code

Chapter III: Program Construction

1. Introduction to the mathematics of program construction
   • The specification / implementation dichotomy. Abstract modeling.
   • Correct by verification versus correct by construction.
2. Description versus calculation
3. The Point-free (PF) transform
   • Taxonomy of binary relations; simple relations and their role in abstract modeling
   • Point-free notation and reasoning
   • Rules of the PF-transform
   • Categorical and allegorical foundations
4. Universal properties and Galois connections
   • Universal constructions and properties; natural properties
   • Reynolds? relation and the free-theorem of polymorphism
   • Galois connections and their corollaries
5. Reasoning by PF-calculation
   • PF-calculation of the consistency of a formal model: satisfiability and invariance
   • Data-level calculation: representing and abstracting data models.
6. Inductive program calculation
   • Relational hylomorphisms
   • Fixpoint calculus and Galois connections: the fixpoint fusion theorem
   • Calculating recursive solutions for hylo-equations
7. Open issues and hot topics in the mathematics of program construction

50 Recent Changes in TWiki Web retrieved at 17:33 (GMT)

See also: RSS feed, recent changes with 50, 100, 200, 500, 1000 topics, all changes

RSD - Rigorous Software Development

(Program Semantics, Verification, and Construction)

Overview.

The reliability of computing systems plays an essential role in modern society, where so many areas of human activity depend on technology. The deliverables of software projects may no longer be limited to code; the ability to produce certified code is now crucial. Code may be certified as being functionally correct, or as possessing certain execution properties (for instance, a program may be certified as not trying to access unauthorised resources).

The ability to certify software in this way requires a sound knowledge of the theory of programming languages and mathematical reasoning tools, as well as acquaintance with tool-assisted techniques. This course gives an overview of the theory of programming languages at an advanced level and then goes on to apply the theory to methods for obtaining correct, certified software.

Aims.

• to present in a systematic way a vast set of results in fundamental areas of Theoretical Computer Science, in particular Logic, Lambda-calculus, Type Theory and Programming Language Semantics, as well as the relationships between them;
• to introduce several rigorous approaches to the production of correct software, namely in:
  • Program Verification , the activity that aims to establish that a program effectively behaves according to its specification, or that its behaviour is characterised by a set of given properties;
  • in Mathematical Program Construction , a method for obtaining correct programs from specifications, strongly based on program calculation.

Lecturing Team.

The team consists of members of the Department of Informatics of the University of Minho and the Department of Computer Science of the University of Porto (Faculty of Science). All team members are working, and have worked actively in the past few years, on topics that are directly related to the subjects covered by this course, as detailed below.

• José Bacelar Almeida (DI-UM) has worked on the verification of security protocols, and has experience in using proof-assistants for program development.
• Sabine Broda (DCC-FCUP) has worked on Mathematical Logic, lambda-calculus, and Type Theory.
• Mário Florido (DCC-FCUP) has worked on lambda-calculus, type systems, and program transformation.
• Maria J. Frade (DI-UM) has worked on lambda-calculus, type systems, and Proof Theory.
• Nelma Moreira (DCC-FCUP) has worked on Automata Theory, Proof Theory, and proof assistants.
• José N. Oliveira (DI-UM) has worked extensively on Formal Methods in Software Engineering and is a pioneer of this area in Portugal.
• Jorge Sousa Pinto (DI-UM) has worked on Linear Logic, lambda-calculus, and functional program transformation.

• Education/MapiFc Web
• Create New Topic
• Index
• Search
• Changes
• Notifications
• Statistics
• Preferences

• Main Webs

•  DI
•  EL
•  Education
•  Events
•  JoseLuisSilva
•  Personal
•  Research

Education/MapiFc Web Preferences

The following settings are web preferences of the Education.MapiFc web. These preferences overwrite the site-level preferences in TWiki.TWikiPreferences and Main.TWikiPreferences, and can be overwritten by user preferences (your personal topic, eg: TWikiGuest in the Main web).

Web Parameters

• Set ANO_DEF = 0809

Web Preferences Settings

Preferences:

• Set SKIN=nat

• Set SKINSTYLE = Kubrick
• Set STYLEBORDER = thin
• Set STYLEBUTTONS = off
• Set STYLESIDEBAR = left
• Set STYLEVARIATION = none
• Set STYLESEARCHBOX = off

• Set PAGETITLE = MAP/i - Foundations of Computing

• Set NATWEBLOGO = MAP/i - Foundations of Computing
• Set WEBLOGOALT = Option I: Program Semantics, Verification, and Construction
• Set WEBLOGOURL = WebHome

• Set WEBCOPYRIGHT = Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.

• List of topics of the Education/MapiFc web:
  • #Set WEBTOPICLIST = Changes | Index | Search | Go

• Web-specific background color: (Pick a lighter one of the StandardColors).
  • Set WEBBGCOLOR = #D0D0D0
  • Note: This setting is automatically configured when you create a web

• Image, URL and alternate tooltip text of web's logo.
  Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.
  • #Set WEBLOGOIMG = /twiki/pub/Main/LocalLogos/um_eengP.jpg
  • #Set WEBLOGOURL = WebHome
  • #Set WEBLOGOALT = Option I: Program Semantics, Verification, and Construction

• List of topics of the TWiki.Education/MapiFc web:
  • Set WEBTITLE = MAP/i - Foundations of Computing

• List this web in the SiteMap:
  • If yes, Set SITEMAPLIST = on, and add the "what" and "use to..." description for the site map. Make sure to list only links that include the name of the web, e.g. Education/MapiFc.Topic links.
  • Set SITEMAPLIST = on
  • Set SITEMAPWHAT = MAP/i - Foundations of Computing
  • Set SITEMAPUSETO = Option I: Program Semantics, Verification, and Construction

• Exclude web from a web="all" search: (Set to on for hidden webs)
  • Set NOSEARCHALL =

• Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
  • #Set NOAUTOLINK =
  • Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.

• Default template for new topics for this web:
  • WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
  • TWiki.WebTopicEditTemplate: Site-level default topic template

• Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
  • Set WEBFORMS =

• Users or groups who are not / are allowed to view / change / rename topics in the Education/MapiFc web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
  • #Set DENYWEBVIEW =
  • #Set ALLOWWEBVIEW =
  • #Set DENYWEBCHANGE =
  • #Set ALLOWWEBCHANGE = TWikiAdminGroup
  • #Set DENYWEBRENAME =
  • #Set ALLOWWEBRENAME = TWikiAdminGroup

• Users or groups allowed to change or rename this WebPreferences topic: (e.g., TWikiAdminGroup)
  • #Set ALLOWTOPICCHANGE = TWikiAdminGroup
  • Set ALLOWTOPICRENAME = TWikiAdminGroup

• Web preferences that are not allowed to be overridden by user or topic preferences:
  • Set FINALPREFERENCES = NOSEARCHALL, ATTACHFILESIZELIMIT, WIKIWEBMASTER, WEBCOPYRIGHT, WEBTOPICLIST, DENYWEBVIEW, ALLOWWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME

Help on Preferences

• A preference setting is defined by:
  3 or 6 spaces * Set NAME = value
  Example:
  • Set WEBBGCOLOR = #FFFFC0
• A preferences setting can be disabled with a # sign. Remove the # sign to enable a local customisation. Example:
  
  • #Set DENYWEBCHANGE = UnknownUser
• Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
  • When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
• The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
• You can introduce your own preferences variables and use them in your topics and templates.

Related Topics

• TWiki.TWikiPreferences, Main.TWikiPreferences - site-level preferences
• TWikiUsers - list of user topics. User topics can have optional user preferences
• TWikiVariables - list of common %VARIABLES%
• TWikiAccessControl - explains how to restrict access by users or groups

Tools

• Rename, move or delete this web:
  • Rename/move/delete web..., looking for references in all public webs - See also: ManagingWebs

Web Search

Search: \.*

Overview
Recommended Books
Syllabus and Course Material
Assessment